Skip to content
Snippets Groups Projects
Commit 0382b116 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'feature/aorai/normalize-bool-operators' into 'master'

Avoid using logical operators in C code in Aoraï instrumentation

See merge request frama-c/frama-c!3020
parents 07385b9d 3bf18118
No related branches found
No related tags found
No related merge requests found
Showing
with 390 additions and 70 deletions
......@@ -1982,8 +1982,45 @@ let mk_transitions_stmt generated_kf loc f st res trans =
trans
([],[],Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc, [])
let mk_goto loc b =
let ghost = true in
match b.bstmts with
| [] -> Cil.mkBlock []
| [ { skind = Instr i } ] ->
let s = mkStmtOneInstr ~ghost i in
Cil.mkBlock [s]
| [ { skind = Goto (s,_) }] ->
let s' = mkStmt ~ghost (Goto (ref !s,loc)) in
Cil.mkBlock [s']
| s::_ ->
s.labels <-
(Label(Data_for_aorai.get_fresh "__aorai_label",loc,false)):: s.labels;
let s' = mkStmt ~ghost (Goto (ref s,loc)) in
Cil.mkBlock [s']
let normalize_condition loc cond block1 block2 =
let rec aux cond b1 b2 =
match cond.enode with
| UnOp(LNot,e,_) -> aux e b2 b1
| BinOp(LAnd,e1,e2,_) ->
let b2' = mk_goto loc b2 in
let b1'= Cil.mkBlock [aux e2 b1 b2'] in
aux e1 b1' b2
| BinOp(LOr,e1,e2,_) ->
let b1' = mk_goto loc b1 in
let b2' = Cil.mkBlock [aux e2 b1' b2] in
aux e1 b1 b2'
| _ ->
Cil.mkStmt ~ghost:true (If(cond,b1,b2,loc))
in
aux cond block1 block2
let mkIfStmt loc exp1 block1 block2 =
Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
if Kernel.LogicalOperators.get() then
Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
else
normalize_condition loc exp1 block1 block2
let mk_deterministic_stmt
generated_kf loc auto f fst status ret state
......
......@@ -111,6 +111,8 @@ let extend () =
if ProveAuxSpec.get () then begin
if InternalWpShare.is_set() then
Wp.Wp_parameters.Share.set (InternalWpShare.get());
Wp.Wp_parameters.Split.on();
Wp.Wp_parameters.SplitMax.set 32;
Wp.Wp_parameters.Verbose.set 0;
Globals.Functions.iter check_auto_func;
end else begin
......
......@@ -52,8 +52,9 @@ extern int call_to_an_undefined_function(void);
T0_S2_tmp = T0_S2;
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
if (T0_S2 == 1 || accept_S1 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......@@ -160,7 +161,9 @@ int a(void)
accept_S1_tmp = accept_S1;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1 || accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......
......@@ -274,10 +274,12 @@ int commit_trans(void)
accept_S4_tmp = accept_S4;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1;
if (accept_S2 == 1)
if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0;
else accept_S4_tmp = 0;
accept_S3_tmp = 0;
if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1;
if (accept_S2 == 1)
if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0;
else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
......
......@@ -145,7 +145,9 @@ int rr = 1;
accept_all_tmp = 0;
accept_S5_tmp = 0;
accept_S4_tmp = 0;
if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
if (T0_S2 == 1)
if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
else accept_S3_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -238,7 +238,9 @@ void opa(void)
accept_S3_tmp = accept_S3;
accept_all_tmp = accept_all;
accept_all_tmp = 0;
if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
if (T1_S2 == 1)
if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
else accept_S3_tmp = 0;
T1_S2_tmp = 0;
T0_init_tmp = 0;
T0_S4_tmp = 0;
......
......@@ -219,8 +219,9 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if (accept_S1 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
......@@ -268,10 +269,12 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if (accept_S1 == 1 || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
if (accept_S1 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
accept_init = accept_init_tmp;
......
......@@ -106,7 +106,11 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
if (S1 == 1) S1_tmp = 1;
else
if (T1 == 1)
if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
......
......@@ -106,7 +106,11 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
if (S1 == 1) S1_tmp = 1;
else
if (T1 == 1)
if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
......@@ -420,7 +424,9 @@ int sumOne(char *t, int length)
T0_init_tmp = T0_init;
T1_tmp = T1;
accept_T2_tmp = accept_T2;
if (T1 == 1 && res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
if (T1 == 1)
if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
else accept_T2_tmp = 0;
if (T1 == 1) T1_tmp = 1; else T1_tmp = 0;
T0_init_tmp = 0;
S1_tmp = 0;
......
......@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......@@ -250,10 +252,14 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
if (T0_S2 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......@@ -248,10 +250,14 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
if (T0_S2 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -58,7 +58,9 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1;
else
if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
......@@ -255,10 +257,14 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
else accept_S1_tmp = 0;
if (T0_S2 == 1) accept_S2_tmp = 1;
else
if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
if (T0_S2 == 1) accept_S1_tmp = 1;
else
if (accept_S1 == 1) accept_S1_tmp = 1;
else
if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
......
......@@ -3,5 +3,5 @@
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:86: Warning:
[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:87: Warning:
Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
void main(int x) {
f(x);
}
%init : I;
I: { f().x == 1 } -> I | other -> I;
......@@ -42,8 +42,15 @@ enum aorai_OpStatusList {
aorai_CurOperation = op_main;
S0_tmp = S0;
S1_tmp = S1;
if (S0 == 1 && s->x >= 0 || S0 == 1 && s->x < 0) S1_tmp = 1;
else S1_tmp = 0;
if (S0 == 1) {
if (s->x >= 0) S1_tmp = 1; else goto __aorai_label;
}
else {
__aorai_label: ;
if (S0 == 1)
if (s->x < 0) S1_tmp = 1; else S1_tmp = 0;
else S1_tmp = 0;
}
S0_tmp = 0;
S0 = S0_tmp;
S1 = S1_tmp;
......
......@@ -112,10 +112,16 @@ check lemma S0_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
else
if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
if (3 == aorai_CurStates) {
if (x == 4) aorai_CurStates = S4; else goto __aorai_label;
}
else {
__aorai_label: ;
if (3 == aorai_CurStates)
if (x == 5) aorai_CurStates = S5;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
}
return;
}
......@@ -241,7 +247,8 @@ void g(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
if (1 == aorai_CurStates)
if (x == 4) aorai_CurStates = S3; else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
return;
}
......@@ -292,7 +299,11 @@ void g(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
if (1 == aorai_CurStates)
if (res == 0)
if (X == 5) aorai_CurStates = S2;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
return;
}
......@@ -368,10 +379,16 @@ int f(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
else
if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
if (0 == aorai_CurStates) {
if (c != 0) aorai_CurStates = S1; else goto __aorai_label_0;
}
else {
__aorai_label_0: ;
if (0 == aorai_CurStates)
if (c == 0) aorai_CurStates = S2;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
}
return;
}
......
......@@ -131,16 +131,23 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
if (7 == aorai_CurStates && x == 1) {
aorai_CurStates = aorai_intermediate_state;
aorai_x = x;
}
else
if (7 == aorai_CurStates && x == 3) {
aorai_CurStates = aorai_intermediate_state_2;
aorai_x_0 = x;
if (7 == aorai_CurStates) {
if (x == 1) {
aorai_CurStates = aorai_intermediate_state;
aorai_x = x;
}
else goto __aorai_label;
}
else {
__aorai_label: ;
if (7 == aorai_CurStates)
if (x == 3) {
aorai_CurStates = aorai_intermediate_state_2;
aorai_x_0 = x;
}
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
}
return;
}
......@@ -214,14 +221,30 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK;
else
if (1 == aorai_CurStates && aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
else
if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject;
else
if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject;
if (4 == aorai_CurStates) {
if (aorai_x_0 == 3) aorai_CurStates = OK; else goto __aorai_label_2;
}
else {
__aorai_label_2: ;
if (1 == aorai_CurStates) {
if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
else goto __aorai_label_1;
}
else {
__aorai_label_1: ;
if (4 == aorai_CurStates) {
if (aorai_x_0 != 3) aorai_CurStates = aorai_reject;
else goto __aorai_label_0;
}
else {
__aorai_label_0: ;
if (1 == aorai_CurStates)
if (aorai_x != 1) aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
}
}
}
return;
}
......@@ -422,14 +445,20 @@ int f(int x)
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
else
if (3 == aorai_CurStates) {
if (aorai_y == 2) aorai_CurStates = OK; else goto __aorai_label_3;
}
else {
__aorai_label_3: ;
if (0 == aorai_CurStates) aorai_CurStates = OK;
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject;
if (3 == aorai_CurStates)
if (aorai_y != 2) aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
}
return;
}
......
......@@ -317,10 +317,14 @@ int main_bhv_bhv(int c); */
aorai_reject_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1;
if (S0 == 1)
if (c <= 0) aorai_intermediate_state_0_tmp = 1;
else aorai_intermediate_state_0_tmp = 0;
else aorai_intermediate_state_0_tmp = 0;
bhv_aux = main_bhv_bhv(c);
if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1;
if (S0 == 1)
if (bhv_aux) aorai_intermediate_state_tmp = 1;
else aorai_intermediate_state_tmp = 0;
else aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
S0_tmp = 0;
......@@ -409,17 +413,25 @@ int main_bhv_bhv(int c); */
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_reject_tmp = aorai_reject;
if ((aorai_intermediate_state_0 == 1 || aorai_intermediate_state_2 == 1 &&
res != 0) || aorai_reject == 1)
aorai_reject_tmp = 1;
else aorai_reject_tmp = 0;
if (aorai_intermediate_state_0 == 1) aorai_reject_tmp = 1;
else
if (aorai_intermediate_state_2 == 1) {
if (res != 0) aorai_reject_tmp = 1; else goto __aorai_label;
}
else {
__aorai_label: ;
if (aorai_reject == 1) aorai_reject_tmp = 1;
else aorai_reject_tmp = 0;
}
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 &&
res == 0) Sf_tmp = 1;
else Sf_tmp = 0;
if (aorai_intermediate_state == 1) Sf_tmp = 1;
else
if (aorai_intermediate_state_2 == 1)
if (res == 0) Sf_tmp = 1; else Sf_tmp = 0;
else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
......
[kernel] Parsing tests/ya/logical_operators.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 1,
op_main = 0
};
enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
/*@ ghost enum aorai_ListOper aorai_CurOperation; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
/*@ ghost int I = 1; */
/*@ ghost
/@ requires 1 ≡ I;
requires 1 ≡ I ⇒ x ≡ 1 ∨ x ≢ 1;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ I ∧ (x ≡ 1 ∨ x ≢ 1);
ensures 1 ≡ I;
behavior buch_state_I_out:
assumes 0 ≡ I ∨ (¬(x ≡ 1) ∧ ¬(x ≢ 1));
ensures 0 ≡ I;
@/
void f_pre_func(int x)
{
int I_tmp;
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
I_tmp = I;
if (I == 1) {
if (x != 1) I_tmp = 1; else goto __aorai_label;
}
else {
__aorai_label: ;
if (I == 1)
if (x == 1) I_tmp = 1; else I_tmp = 0;
else I_tmp = 0;
}
I = I_tmp;
return;
}
*/
/*@ ghost
/@ requires 1 ≡ I;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ I;
ensures 1 ≡ I;
behavior buch_state_I_out:
assumes 0 ≡ I;
ensures 0 ≡ I;
@/
void f_post_func(void)
{
int I_tmp;
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
I_tmp = I;
if (I == 1) I_tmp = 1; else I_tmp = 0;
I = I_tmp;
return;
}
*/
/*@ requires 1 ≡ I;
requires 1 ≡ I ⇒ x ≡ 1 ∨ x ≢ 1;
behavior Buchi_property_behavior:
ensures \true;
ensures 1 ≡ I;
*/
void f(int x)
{
/*@ ghost f_pre_func(x); */
/*@ ghost f_post_func(); */
return;
}
/*@ ghost
/@ requires 1 ≡ I;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ I;
ensures 1 ≡ I;
behavior buch_state_I_out:
assumes 0 ≡ I;
ensures 0 ≡ I;
@/
void main_pre_func(int x)
{
int I_tmp;
/@ slevel full; @/
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
I_tmp = I;
if (I == 1) I_tmp = 1; else I_tmp = 0;
I = I_tmp;
return;
}
*/
/*@ ghost
/@ requires 1 ≡ I;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, I;
behavior buch_state_I_in:
assumes 1 ≡ I;
ensures 1 ≡ I;
behavior buch_state_I_out:
assumes 0 ≡ I;
ensures 0 ≡ I;
@/
void main_post_func(void)
{
int I_tmp;
/@ slevel full; @/
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
I_tmp = I;
if (I == 1) I_tmp = 1; else I_tmp = 0;
I = I_tmp;
return;
}
*/
/*@ requires 1 ≡ I;
behavior Buchi_property_behavior:
ensures \true;
ensures 1 ≡ I;
*/
void main(int x)
{
/*@ ghost main_pre_func(x); */
f(x);
/*@ ghost main_post_func(); */
return;
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment