Mentions légales du service

Skip to content
Snippets Groups Projects
Commit abdd9789 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Jessie3: update regression tests

parent 801703f9
No related branches found
No related tags found
No related merge requests found
let help = "Checks ACSL contracts using Why3" let help = "Checks ACSL contracts using Why3"
let global_logic_decls_theory_name = "Global logic declarations"
let programs_module_name = "C Functions"
module Self = module Self =
Plugin.Register Plugin.Register
(struct (struct
...@@ -413,7 +421,10 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) = ...@@ -413,7 +421,10 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
Self.not_yet_implemented "Dlemma with labels or vars" Self.not_yet_implemented "Dlemma with labels or vars"
end end
| Daxiomatic (name, decls', loc) -> | Daxiomatic (name, decls', loc) ->
let theories = add_decls_as_theory theories (Ident.id_fresh "Top") decls in let theories =
add_decls_as_theory theories
(Ident.id_fresh global_logic_decls_theory_name) decls
in
let (t,decls'') = let (t,decls'') =
List.fold_left List.fold_left
(fun acc d -> logic_decl ~in_axiomatic:true d loc acc) (fun acc d -> logic_decl ~in_axiomatic:true d loc acc)
...@@ -452,14 +463,8 @@ let seq e1 e2 = ...@@ -452,14 +463,8 @@ let seq e1 e2 =
let annot a e = let annot a e =
match (Annotations.code_annotation_of_rooted a).annot_content with match (Annotations.code_annotation_of_rooted a).annot_content with
| AAssert ([],pred) -> | AAssert ([],pred) ->
(**)
Self.result "annot AAssert";
(**)
let p = predicate_named pred in let p = predicate_named pred in
let a = Mlw_expr.e_assert Mlw_expr.Aassert p in let a = Mlw_expr.e_assert Mlw_expr.Aassert p in
(**)
Self.result "annot AAssert, make seq";
(**)
seq a e seq a e
| AAssert(_labels,_pred) -> | AAssert(_labels,_pred) ->
Self.not_yet_implemented "annot AAssert" Self.not_yet_implemented "annot AAssert"
...@@ -493,7 +498,6 @@ let instr i = ...@@ -493,7 +498,6 @@ let instr i =
let stmt s = let stmt s =
match s.skind with match s.skind with
| Instr i -> | Instr i ->
Self.result "annot AAssert, make seq";
let annotations = Annotations.code_annot s in let annotations = Annotations.code_annot s in
let e = let e =
List.fold_right annot annotations (instr i) List.fold_right annot annotations (instr i)
...@@ -705,10 +709,13 @@ let prog p = ...@@ -705,10 +709,13 @@ let prog p =
in in
Self.result "found %d logic decl(s)" (List.length decls); Self.result "found %d logic decl(s)" (List.length decls);
let theories = let theories =
add_decls_as_theory theories (Ident.id_fresh "Jessie3 Top") decls add_decls_as_theory theories
(Ident.id_fresh global_logic_decls_theory_name) decls
in in
Self.result "made %d theory(ies)" (List.length theories); Self.result "made %d theory(ies)" (List.length theories);
let m = Mlw_module.create_module env (Ident.id_fresh "Jessie3 Program") in let m = Mlw_module.create_module env
(Ident.id_fresh programs_module_name)
in
let m = use m int_theory in let m = use m int_theory in
let m = use m real_theory in let m = use m real_theory in
let m = List.fold_left use m theories in let m = List.fold_left use m theories in
......
...@@ -7,17 +7,17 @@ ...@@ -7,17 +7,17 @@
@ type bag<X>; @ type bag<X>;
@ logic integer occ<X>(X x, bag<X> b); @ logic integer occ<X>(X x, bag<X> b);
@ // axiom extensionality<X>: \forall bag<X> b1,b2; @ // axiom extensionality<X>: \forall bag<X> b1,b2;
@ // (\forall X x; occ(x,b1) == occ(x,b2)) ==> b1 == b2; @ // (\forall X x; occ(x,b1) == occ(x,b2)) ==> b1 == b2;
@ logic bag<X> empty<X>; @ // logic bag<X> empty<X>;
@ @
@ logic bag<X> singleton<X>(X x); @ logic bag<X> singleton<X>(X x);
@ // axiom occ_singleton_eq<X>: \forall X x; @ // axiom occ_singleton_eq<X>: \forall X x;
@ // occ(x,singleton(x)) == 1; @ // occ(x,singleton(x)) == 1;
@ // axiom occ_singleton_neq<X>: \forall X x,y; @ // axiom occ_singleton_neq<X>: \forall X x,y;
@ // x != y ==> occ(x,singleton(y)) == 0; @ // x != y ==> occ(x,singleton(y)) == 0;
@ logic bag<X> bag_union<X>(bag<X> b1,bag<X> b2); @ logic bag<X> bag_union<X>(bag<X> b1,bag<X> b2);
@ // axiom occ_union<X>: \forall X x, bag<X> b1,b2; @ // axiom occ_union<X>: \forall X x, bag<X> b1,b2;
@ // occ(x,bag_union(b1,b2)) == occ(x,b1) + occ(x,b2); @ // occ(x,bag_union(b1,b2)) == occ(x,b1) + occ(x,b2);
@ } @ }
@*/ @*/
......
...@@ -5,10 +5,11 @@ ...@@ -5,10 +5,11 @@
[jessie3] creating logic symbol 743 (occ) [jessie3] creating logic symbol 743 (occ)
[jessie3] creating logic symbol 748 (singleton) [jessie3] creating logic symbol 748 (singleton)
[jessie3] creating logic symbol 754 (bag_union) [jessie3] creating logic symbol 754 (bag_union)
[jessie3] found 1 decls [jessie3] found 1 logic decl(s)
[jessie3] made 3 theories [jessie3] made 3 theory(ies)
[jessie3] made 0 function(s)
[jessie3] running theory 1: [jessie3] running theory 1:
[jessie3] theory Top [jessie3] theory Global_logic_declarations
(* use BuiltIn *) (* use BuiltIn *)
(* use int.Int *) (* use int.Int *)
...@@ -33,7 +34,7 @@ ...@@ -33,7 +34,7 @@
(* use real.Real *) (* use real.Real *)
(* use Top *) (* use Global_logic_declarations *)
type bag type bag
...@@ -64,7 +65,7 @@ ...@@ -64,7 +65,7 @@
[jessie3] Status with Z3 3.2: Valid [jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid [jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] running theory 1: [jessie3] running theory 1:
[jessie3] theory Top1 [jessie3] theory Global_logic_declarations1
(* use BuiltIn *) (* use BuiltIn *)
(* use int.Int *) (* use int.Int *)
...@@ -81,3 +82,19 @@ ...@@ -81,3 +82,19 @@
[jessie3] Status with Z3 4.0: Valid [jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid [jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Unknown [jessie3] Status with Alt-Ergo 0.94: Unknown
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use Bool *)
(* use Unit *)
(* use Prelude *)
(* use int.Int *)
(* use real.Real *)
(* use Global_logic_declarations1 *)
end
...@@ -2,5 +2,28 @@ ...@@ -2,5 +2,28 @@
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated [jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated [jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] processing function f [jessie3] processing function f
[jessie3] found 0 decls [jessie3] found 0 logic decl(s)
[jessie3] made 0 theories [jessie3] made 0 theory(ies)
[jessie3] made 1 function(s)
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use Bool *)
(* use Unit *)
(* use Prelude *)
(* use int.Int *)
(* use real.Real *)
goal WP_parameter_f : (6 * 7) = 42
end
[jessie3] Dealing with task 1
[jessie3] Status with CVC3 2.4.1: Valid
[jessie3] Status with CVC3 2.2: Valid
[jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid
[kernel] preprocessing with "gcc -C -E -I. tests/basic/generic.c" [kernel] preprocessing with "gcc -C -E -I. tests/basic/generic.c"
tests/basic/generic.c:15:[kernel] user error: unbound function f1 in annotation. [jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[kernel] user error: skipping file "tests/basic/generic.c" that has errors. [jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[kernel] Frama-C aborted: invalid user input. [jessie3] creating logic symbol 740 (occ)
[jessie3] creating logic symbol 742 (singleton)
[jessie3] creating logic symbol 745 (bag_union)
[jessie3] found 0 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
[jessie3] running theory 1:
[jessie3] theory Bag
(* use BuiltIn *)
(* use int.Int *)
(* use real.Real *)
type bag 'x
function occ 'x (bag 'x) : int
function singleton 'x : bag 'x
function bag_union (bag 'x) (bag 'x) : bag 'x
end
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use Bool *)
(* use Unit *)
(* use Prelude *)
(* use int.Int *)
(* use real.Real *)
(* use Bag *)
end
[kernel] preprocessing with "gcc -C -E -I. tests/basic/lemma.c" [kernel] preprocessing with "gcc -C -E -I. tests/basic/lemma.c"
[jessie3] user error: WARNING: Variable Frama_C_bzero not translated [jessie3] user error: WARNING: Variable Frama_C_bzero not translated
[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated [jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
[jessie3] found 7 decls [jessie3] found 7 logic decl(s)
[jessie3] made 1 theories [jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
[jessie3] running theory 1: [jessie3] running theory 1:
[jessie3] theory Top [jessie3] theory Global_logic_declarations
(* use BuiltIn *) (* use BuiltIn *)
(* use int.Int *) (* use int.Int *)
...@@ -67,3 +68,19 @@ ...@@ -67,3 +68,19 @@
[jessie3] Status with Z3 4.0: Valid [jessie3] Status with Z3 4.0: Valid
[jessie3] Status with Z3 3.2: Valid [jessie3] Status with Z3 3.2: Valid
[jessie3] Status with Alt-Ergo 0.94: Valid [jessie3] Status with Alt-Ergo 0.94: Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use BuiltIn *)
(* use Bool *)
(* use Unit *)
(* use Prelude *)
(* use int.Int *)
(* use real.Real *)
(* use Global_logic_declarations *)
end
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment