Commit 464006e1 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Jessie3: back to attempt on using dexpr

parent 7ba28dc5
This diff is collapsed.
This diff is collapsed.
......@@ -29,6 +29,9 @@ Jessie3.cmx: $(addsuffix .cmx, $(MODULES))
Jessie3.cmxs: Jessie3.cmx
ocamlopt.opt -shared $(FLAGS) $(INCLUDE) -o $@ $(addsuffix .cmx, @MENHIRLIB@) $(addsuffix .cmxa, @ZIPLIB@) $(WHYLIB)/why3.cmxa $^
%.cmi: %.mli
ocamlc.opt $(FLAGS) $(INCLUDE) -c $^
%.cmo: %.ml
ocamlc.opt $(FLAGS) $(INCLUDE) -c $^
......@@ -61,10 +64,11 @@ tests/ptests_config: Makefile
chmod a-w tests/ptests_config
clean:
rm -f $(addsuffix .cmi, $(MODULES))
rm -f $(addsuffix .cmo, $(MODULES))
rm -f $(addsuffix .cmx, $(MODULES))
rm -f Jessie3.cma Jessie3.cmxs
register.cmx: ACSLtoWhy3.cmx
register.cmo: ACSLtoWhy3.cmi
register.cmo: ACSLtoWhy3.cmo
......@@ -26,7 +26,7 @@ open Why3
let () = Debug.set_flag Call_provers.debug
*)
let limit = Call_provers.{ limit_time = 3 ;
let limit = Call_provers.{ limit_time = 1 ;
limit_mem = 1000;
limit_steps = -1;}
......@@ -73,11 +73,9 @@ let process () =
List.fold_left
(get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
[]
[ "Z432", "Z3,4.3.2,";
"Z440", "Z3,4.4.0,";
"C241", "CVC3,2.4.1,";
[ "Z441", "Z3,4.4.1,";
"C414", "CVC4,1.4,";
"A991", "Alt-Ergo,0.99.1,";
"A101", "Alt-Ergo,1.01,";
]
with e ->
ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a"
......@@ -104,12 +102,20 @@ let process () =
Format.fprintf fmt "%s %s" p.Whyconf.prover_name p.Whyconf.prover_version))
provers;
let _ =
List.fold_left (fun n t ->
let g = Task.task_goal t in
ACSLtoWhy3.Self.result "@[<h 0>Task %d (%s): %a@]" n g.Decl.pr_name.Ident.id_string
(Pp.print_list Pp.comma (fun fmt (_n,p,d) -> run_on_task fmt p d t))
provers;
n+1) 1 tasks
List.fold_left
(fun n t ->
let l = Trans.apply_transform "split_goal_wp" ACSLtoWhy3.env t in
List.fold_left
(fun n t ->
let (g,expl,t) = Termcode.goal_expl_task ~root:false t in
ACSLtoWhy3.Self.result
"@[<h 0>Task %d (%s) (%a): %a@]" n g.Ident.id_string
(Pp.print_option Format.pp_print_string) expl
(Pp.print_list Pp.comma (fun fmt (_n,p,d) -> run_on_task fmt p d t))
provers;
n+1)
n l)
1 tasks
in ())
theories
with e ->
......@@ -127,8 +133,8 @@ let (_unused : (unit -> unit) -> unit -> unit) =
let run () = if ACSLtoWhy3.Enabled.get () then process ()
let () =
try
(* try *)
Db.Main.extend run
with e ->
ACSLtoWhy3.Self.fatal "Exception raised when loading Jessie3:@ %a"
Exn_printer.exn_printer e
(* with e -> *)
(* ACSLtoWhy3.Self.fatal "Exception raised when loading Jessie3:@ %a" *)
(* Exn_printer.exn_printer e *)
......@@ -23,8 +23,6 @@ void g(int x) {
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 call.c"
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 call.c"
End:
*/
......@@ -21,8 +21,6 @@
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 constants.c"
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 constants.c"
End:
*/
......@@ -11,12 +11,10 @@ void g(void) {
//@ assert x*7 == 42;
}
// ensures \result == 42;
/*
//@ ensures \result == 42;
int h(void) {
return 6*7;
}
*/
/*
Local Variables:
......
......@@ -2,13 +2,29 @@
OPT: -journal-disable -jessie3
*/
int x = 42;
void f(void) {
//@ assert 6*7 == x;
int x = 6;
int test0(void) {
return x;
}
void test1(void) {
x = 3;
}
const int y = 7;
void f(void) {
// This should be proved
//@ assert 6*y == 42;
// This should not be proved
//@ assert x*7 == 42;
x++;
}
/*
Local Variables:
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 global.c"
......
......@@ -23,8 +23,6 @@ void h(int x) {
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 incr.c"
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 incr.c"
End:
*/
......@@ -26,8 +26,6 @@
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 lemma.c"
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 lemma.c"
End:
*/
......@@ -5,7 +5,7 @@
//@ logic integer sum_upto(integer n) = n*(n+1) / 2;
/*@ lemma sum_rec: \forall integer n; n >=0 ==>
/*@ lemma sum_rec: \forall integer n; n >= 0 ==>
@ sum_upto(n+1) == sum_upto(n)+n+1;
@*/
......@@ -41,6 +41,6 @@ long main () {
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 rec.c"
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 rec.c"
End:
*/
......@@ -444,6 +444,8 @@ type denv = {
locals : (Stv.t option * dvty) Mstr.t;
}
let denv_contents d = d.locals
let denv_empty = { frozen = []; locals = Mstr.empty }
let is_frozen frozen v =
......
......@@ -144,6 +144,8 @@ val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *)
val denv_get_opt : denv -> string -> dexpr_node option
val denv_contents : denv -> (Ty.Stv.t option * dvty) Mstr.t
(** Constructors *)
val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
......
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