Commit af2a5b9d authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update Readme

parent 83db0309
......@@ -90,7 +90,7 @@ the _preconditions_ specified in the contract of the function.
- `-wp-model real+Cast+ref`: enables the `real` model to represent the
arithmetic on floating-point numbers. The `Cast` option enables the
usage of cast in the code. Finally, the `ref` option is used to enable optimization for reference parameters.
- `-wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,tip`:
- `-wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip`:
adds the different provers needed to verify the goals.
' `-wp-check-memory-model`: Insert memory model hypotheses in the function contracts. Necessary as we use the `ref` memory model.
- `-cpp-extra-args=-I../include`: adds the include directory of
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment