[e-acsl] the type system is now working: no more GMP in practice :-D
Showing
- src/plugins/e-acsl/TODO 0 additions, 5 deletionssrc/plugins/e-acsl/TODO
- src/plugins/e-acsl/env.ml 17 additions, 11 deletionssrc/plugins/e-acsl/env.ml
- src/plugins/e-acsl/env.mli 1 addition, 1 deletionsrc/plugins/e-acsl/env.mli
- src/plugins/e-acsl/quantif.ml 20 additions, 24 deletionssrc/plugins/e-acsl/quantif.ml
- src/plugins/e-acsl/quantif.mli 1 addition, 1 deletionsrc/plugins/e-acsl/quantif.mli
- src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i 1 addition, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
- src/plugins/e-acsl/tests/e-acsl-runtime/arith.i 1 addition, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/arith.i
- src/plugins/e-acsl/tests/e-acsl-runtime/at.i 1 addition, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/at.i
- src/plugins/e-acsl/tests/e-acsl-runtime/cast.i 5 additions, 5 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/cast.i
- src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i 1 addition, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
- src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i 1 addition, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle 1 addition, 1 deletion...gins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle 80 additions, 1193 deletions...ugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle 73 additions, 531 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle 38 additions, 79 deletions...lugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle 40 additions, 415 deletions.../e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle 113 additions, 1055 deletions.../tests/e-acsl-runtime/oracle/function_contract.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c 1 addition, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c 37 additions, 443 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c 41 additions, 227 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
Loading
Please register or sign in to comment