From fde36fa19a557f45c17c0cd266fd87a4823e8e6d Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 25 May 2011 14:18:10 +0000
Subject: [PATCH] [e-acsl] use a function type instead of void when required
---
src/plugins/e-acsl/misc.ml | 3 +-
.../oracle/stmt_contract.res.oracle | 256 +++++++++---------
2 files changed, 130 insertions(+), 129 deletions(-)
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index b98f439ed12..585d6530dad 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -45,7 +45,8 @@ let mk_call ?(loc=Location.unknown) ?result fname args =
(* the type is incorrect, but it doesn't matter *)
(* [JS 2011/04/12] should not generate a new variable by function name *)
(* [TODO] require a projectified table to associate an lval to each name *)
- let f = new_lval ~loc (makeGlobalVar fname voidType) in
+ let ty = TFun(voidType, None, false, []) in
+ let f = new_lval ~loc (makeGlobalVar fname ty) in
mkStmt ~valid_sid:true (Instr(Call(result, f, args, loc)))
(* Build a C conditional doing a runtime assertion check. *)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index 750cb1810f1..3f86f8c193f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -39,10 +39,10 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
Called from PROJECT_FILE.i:139.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:139.
+ Called from PROJECT_FILE.i:140.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:140.
+ Called from PROJECT_FILE.i:141.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -52,16 +52,16 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:141.
+ Called from PROJECT_FILE.i:142.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:141.
+ Called from PROJECT_FILE.i:142.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:142.
+ Called from PROJECT_FILE.i:143.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:143.
+ Called from PROJECT_FILE.i:144.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -71,28 +71,28 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:144.
+ Called from PROJECT_FILE.i:145.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:144.
+ Called from PROJECT_FILE.i:145.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:144.
+ Called from PROJECT_FILE.i:145.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:145.
+ Called from PROJECT_FILE.i:146.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:151.
+ Called from PROJECT_FILE.i:152.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:151.
+ Called from PROJECT_FILE.i:152.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:152.
+ Called from PROJECT_FILE.i:153.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:153.
+ Called from PROJECT_FILE.i:154.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -102,22 +102,22 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:154.
+ Called from PROJECT_FILE.i:155.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:154.
+ Called from PROJECT_FILE.i:155.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:161.
+ Called from PROJECT_FILE.i:162.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:162.
+ Called from PROJECT_FILE.i:163.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:162.
+ Called from PROJECT_FILE.i:163.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:163.
+ Called from PROJECT_FILE.i:164.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -127,16 +127,16 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:165.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:164.
+ Called from PROJECT_FILE.i:165.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:165.
+ Called from PROJECT_FILE.i:166.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:166.
+ Called from PROJECT_FILE.i:167.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -146,28 +146,28 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:168.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:168.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:167.
+ Called from PROJECT_FILE.i:168.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:168.
+ Called from PROJECT_FILE.i:169.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:186.
+ Called from PROJECT_FILE.i:187.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:186.
+ Called from PROJECT_FILE.i:187.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:187.
+ Called from PROJECT_FILE.i:188.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:188.
+ Called from PROJECT_FILE.i:189.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -177,29 +177,29 @@ PROJECT_FILE.i:39:[value] Function mpz_clear: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:189.
+ Called from PROJECT_FILE.i:190.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:191.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:190.
+ Called from PROJECT_FILE.i:191.
PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:191.
+ Called from PROJECT_FILE.i:192.
PROJECT_FILE.i:60:[value] Function mpz_add: precondition got status valid
PROJECT_FILE.i:61:[value] Function mpz_add: precondition got status valid
PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] Done for function mpz_add
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:192.
+ Called from PROJECT_FILE.i:193.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:193.
+ Called from PROJECT_FILE.i:194.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -209,16 +209,16 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:194.
+ Called from PROJECT_FILE.i:195.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:194.
+ Called from PROJECT_FILE.i:195.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:195.
+ Called from PROJECT_FILE.i:196.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:196.
+ Called from PROJECT_FILE.i:197.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -228,13 +228,7 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:197.
-[value] Done for function mpz_clear
-[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:197.
-[value] Done for function mpz_clear
-[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:197.
+ Called from PROJECT_FILE.i:198.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:198.
@@ -243,7 +237,7 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
Called from PROJECT_FILE.i:198.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:198.
+ Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:199.
@@ -251,17 +245,23 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:199.
[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:200.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- main.
+ Called from PROJECT_FILE.i:200.
+[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:204.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:204.
+ Called from PROJECT_FILE.i:205.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:205.
+ Called from PROJECT_FILE.i:206.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:206.
+ Called from PROJECT_FILE.i:207.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -271,25 +271,25 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:207.
+ Called from PROJECT_FILE.i:208.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:208.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:208.
+ Called from PROJECT_FILE.i:209.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:209.
+ Called from PROJECT_FILE.i:210.
[value] Done for function mpz_add
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:210.
+ Called from PROJECT_FILE.i:211.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:211.
+ Called from PROJECT_FILE.i:212.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -299,50 +299,50 @@ PROJECT_FILE.i:62:[value] Function mpz_add: precondition got status valid
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:213.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:213.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:212.
+ Called from PROJECT_FILE.i:213.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:214.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:214.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:213.
+ Called from PROJECT_FILE.i:214.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:235.
+ Called from PROJECT_FILE.i:236.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:237.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:237.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:242.
+ Called from PROJECT_FILE.i:243.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:243.
+ Called from PROJECT_FILE.i:244.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:244.
+ Called from PROJECT_FILE.i:245.
[value] Done for function mpz_cmp
-PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:246:[value] assigning non deterministic value for the first time
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:246.
+ Called from PROJECT_FILE.i:247.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:247.
+ Called from PROJECT_FILE.i:248.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:248.
+ Called from PROJECT_FILE.i:249.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -352,46 +352,46 @@ PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:249.
+ Called from PROJECT_FILE.i:250.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:249.
+ Called from PROJECT_FILE.i:250.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:250.
+ Called from PROJECT_FILE.i:251.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:255.
+ Called from PROJECT_FILE.i:256.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:256.
+ Called from PROJECT_FILE.i:257.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:257.
+ Called from PROJECT_FILE.i:258.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:259.
+ Called from PROJECT_FILE.i:260.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:260.
+ Called from PROJECT_FILE.i:261.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:266.
+ Called from PROJECT_FILE.i:267.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:267.
+ Called from PROJECT_FILE.i:268.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:268.
+ Called from PROJECT_FILE.i:269.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:270.
+ Called from PROJECT_FILE.i:271.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:271.
+ Called from PROJECT_FILE.i:272.
[value] Done for function mpz_clear
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:272.
+ Called from PROJECT_FILE.i:273.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -401,50 +401,47 @@ PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:274.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:274.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:274.
+ Called from PROJECT_FILE.i:275.
[value] Done for function mpz_cmp
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:279.
+ Called from PROJECT_FILE.i:280.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:280.
+ Called from PROJECT_FILE.i:281.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:281.
+ Called from PROJECT_FILE.i:282.
[value] Done for function mpz_cmp
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:283.
+ Called from PROJECT_FILE.i:284.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:284.
+ Called from PROJECT_FILE.i:285.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:292.
+ Called from PROJECT_FILE.i:293.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:293.
+ Called from PROJECT_FILE.i:294.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:294.
+ Called from PROJECT_FILE.i:295.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:295.
+ Called from PROJECT_FILE.i:296.
[value] Done for function mpz_add
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:296.
+ Called from PROJECT_FILE.i:297.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:297.
+ Called from PROJECT_FILE.i:298.
[value] Done for function mpz_cmp
-[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:299.
-[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:300.
[value] Done for function mpz_clear
@@ -454,8 +451,11 @@ PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:302.
[value] Done for function mpz_clear
-[value] computing for function e_acsl_fail <- main.
+[value] computing for function mpz_clear <- main.
Called from PROJECT_FILE.i:303.
+[value] Done for function mpz_clear
+[value] computing for function e_acsl_fail <- main.
+ Called from PROJECT_FILE.i:304.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -465,34 +465,34 @@ PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:304.
+ Called from PROJECT_FILE.i:305.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:304.
+ Called from PROJECT_FILE.i:305.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:304.
+ Called from PROJECT_FILE.i:305.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:305.
+ Called from PROJECT_FILE.i:306.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:305.
+ Called from PROJECT_FILE.i:306.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:305.
+ Called from PROJECT_FILE.i:306.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:313.
+ Called from PROJECT_FILE.i:314.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:313.
+ Called from PROJECT_FILE.i:314.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:314.
+ Called from PROJECT_FILE.i:315.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:315.
+ Called from PROJECT_FILE.i:316.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -502,22 +502,22 @@ PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:316.
+ Called from PROJECT_FILE.i:317.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:316.
+ Called from PROJECT_FILE.i:317.
[value] Done for function mpz_clear
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:320.
+ Called from PROJECT_FILE.i:321.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:320.
+ Called from PROJECT_FILE.i:321.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:321.
+ Called from PROJECT_FILE.i:322.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:322.
+ Called from PROJECT_FILE.i:323.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:115.
[value] Done for function printf
@@ -527,10 +527,10 @@ PROJECT_FILE.i:245:[value] assigning non deterministic value for the first time
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:323.
+ Called from PROJECT_FILE.i:324.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:323.
+ Called from PROJECT_FILE.i:324.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
--
GitLab