Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] alt-ergo silently ignored / any idea?

  • Subject: [Frama-c-discuss] alt-ergo silently ignored / any idea?
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Tue, 19 Jun 2012 17:01:51 +0200
Hi,

I am trying to get Nitrogen to work with alt-ergo on MS Windows XP.
Building seems going OK, but when calling wp on the sample source file
from the manual, I can not get an output that indicates that alt-ergo
is actually called.
It seems silently ignored.

alt-ergo ist accessible in PATH and working correctly, as far as I can judge.
Its version is 0.94.

Sample output :
-------------------------------------------------------------------------
$ frama-c -wp  -wp-proof alt-ergo  /c/src/wp.c
[kernel] preprocessing with "gcc -C -E -I.  c:/src/wp.c"
[wp] warning: Missing RTE guards
[wp] [WP:simplified] Goal store_swap_function_assigns : Valid
-------------------------------------------------------------------------
Notice that there is no mention of alt-ergo!

You'll find below the output of "./configure" and of the command above
with "-wp-debug 4".

Please, could somebody hint me at the cause of this behaviour?
Thanks very much in advance,
Sylvain


-------------------------------------------------------------------------
$ ./configure --disable-gui --prefix=/c/frama-c-Nitrogen
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
make version is GNU Make 3.81: Good!
configure: *****************************
configure: * CONFIGURE OCAML COMPILERS *
configure: *****************************
checking for ocamlc... ocamlc
OCaml version is 3.12.1: good!
ocaml library path is C:\Programme\OCaml\lib
checking for ocamlopt... ocamlopt
checking ocamlopt version and standard library... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version and standard library... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version and standard library... ok
configure: *******************************************
configure: * CONFIGURE MANDATORY TOOLS AND LIBRARIES *
configure: *******************************************
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for C:\Programme\OCaml\lib/ocamlgraph/graph.cmx... yes
configure: OcamlGraph 1.8.2 is incompatible with Frama-C.
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph... yes
checking for ocamlgraph.tar.gz... yes
configure: configuring ocamlgraph...
configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph w
ill not be compiled
configure: ******************************************
configure: * CONFIGURE OPTIONAL TOOLS AND LIBRARIES *
configure: ******************************************
checking for ocamldoc... ocamldoc
checking for ocamlmktop... ocamlmktop
checking for otags... no
configure: **********************
configure: * CONFIGURE PLATFORM *
configure: **********************
checking platform... Win32
checking whether performance counters are usable... no (cannot compile perfcount
.c)
configure: ***************************
configure: * WISHED FRAMA-C PLUG-INS *
configure: ***************************
checking for src/constant_propagation... yes
semantic_constant_folding... yes
checking for src/from... yes
from_analysis... yes
checking for src/gui... yes
gui... no
checking for src/impact... yes
impact... yes
checking for src/inout... yes
inout... yes
checking for src/metrics... yes
metrics... yes
checking for src/occurrence... yes
occurrence... yes
checking for src/pdg... yes
pdg... yes
checking for src/postdominators... yes
postdominators... yes
checking for src/rte... yes
rte_annotation... yes
checking for src/scope... yes
scope... yes
checking for src/semantic_callgraph... yes
semantic_callgraph... yes
checking for src/slicing... yes
slicing... yes
checking for src/sparecode... yes
sparecode... yes
checking for src/syntactic_callgraph... yes
syntactic_callgraph... yes
checking for src/users... yes
users... yes
checking for src/value... yes
value_analysis... yes
checking for src/aorai/Makefile.in... yes
aorai... yes
checking for ltl2ba... no
checking for src/report/Makefile.in... yes
report... yes
checking for src/security_slicing/Makefile.in... yes
security_slicing... yes
checking for src/wp/Makefile.in... yes
wp... yes
checking for why... no
checking for why-dp... no
checking for alt-ergo... yes
configure: alt-ergo version is 0.94.
configure: alt-ergo's array theory unsupported.
checking for coqc... no
configure: *******************************************************
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
configure: *******************************************************
checking for C:\Programme\OCaml\lib/lablgtk2/lablgtk.cmxa... no
checking for dot... yes
checking for C:\Programme\OCaml\lib/dynlink.cmxa... yes
native dynlink works fine. Great.
configure: *************************************
configure: * CHECKING FOR PLUG-IN DEPENDENCIES *
configure: *************************************
configure: WARNING: ltl2ba not found.
configure: WARNING: aorai partially enabled because ltl2ba missing.
configure: WARNING: why not found
configure: WARNING: wp partially enabled because why missing.
configure: WARNING: why-dp not found
configure: WARNING: wp partially enabled because why-dp missing.
configure: WARNING: coq not found
configure: WARNING: wp partially enabled because coqc missing.
configure: WARNING: lablgtk2/lablgtk.cmxa not found.
configure: WARNING: impact only partially enabled because gui not enabled.
configure: WARNING: metrics only partially enabled because gui not enabled.
configure: WARNING: occurrence only partially enabled because gui not enabled.
configure: WARNING: scope only partially enabled because gui not enabled.
configure: WARNING: slicing only partially enabled because gui not enabled.
configure: WARNING: syntactic_callgraph only partially enabled because gui not e
nabled.
configure: WARNING: value_analysis only partially enabled because gui not enable
d.
configure: WARNING: security_slicing only partially enabled because gui not enab
led.
configure: WARNING: wp partially enabled because gui not enabled.
configure: *********************
configure: * CREATING MAKEFILE *
configure: *********************
configure: creating ./config.status
config.status: creating src/aorai/Makefile
config.status: creating src/report/Makefile
config.status: creating src/security_slicing/Makefile
config.status: creating src/wp/Makefile
config.status: creating cil/ocamlutil/perfcount.c
config.status: creating share/Makefile.config
configure: *******************************
configure: * SUMMARY: PLUG-INS AVAILABLE *
configure: *******************************
configure: semantic_constant_folding: yes
configure: from_analysis: yes
configure: gui: no
configure: impact: partial, gui not enabled
configure: inout: yes
configure: metrics: partial, gui not enabled
configure: occurrence: partial, gui not enabled
configure: pdg: yes
configure: postdominators: yes
configure: rte_annotation: yes
configure: scope: partial, gui not enabled
configure: semantic_callgraph: yes
configure: slicing: partial, gui not enabled
configure: sparecode: yes
configure: syntactic_callgraph: partial, gui not enabled
configure: users: yes
configure: value_analysis: partial, gui not enabled
configure: aorai: partial, dynamic, ltl2ba missing
configure: report: yes, dynamic
configure: security_slicing: partial, dynamic, gui not enabled
configure: wp: partial, dynamic, gui not enabled
-------------------------------------------------------------------------
[kernel] preprocessing with "gcc -C -E -I.  c:/src/wp.c"
[wp:annot] [get_strategies] for behaviors names: <all>
[wp:cil2cfg] create cfg for function 'swap'
[wp:cil2cfg] add node : <start>
[wp:cil2cfg] add node : <fctIn>
[wp:cil2cfg] add edge : <start> ------> <fctIn>
[wp:cil2cfg] add node : <fctOut>
[wp:cil2cfg] add node : <exit>
[wp:cil2cfg] add node : <end>
[wp:cil2cfg] add edge : <fctOut> ------> <end>
[wp:cil2cfg] add edge : <exit> ------> <end>
[wp:cil2cfg] get_node: <blkIn-fct> --> id:4,0
[wp:cil2cfg] add node : <blkIn-fct>
[wp:cil2cfg] add edge : <blkIn-fct> -(next)-> <fctOut>
[wp:cil2cfg] get_node: <blkOut-fct> --> id:9,0
[wp:cil2cfg] add node : <blkOut-fct>
[wp:cil2cfg] add edge : <blkOut-fct> ------> <fctOut>
[wp:cil2cfg] get_node: <stmt-7> --> id:1,7
[wp:cil2cfg] add node : <stmt-7>
[wp:cil2cfg] add edge : <stmt-7> ------> <blkOut-fct>
[wp:cil2cfg] get_node: <stmt-4> --> id:1,4
[wp:cil2cfg] add node : <stmt-4>
[wp:cil2cfg] add edge : <stmt-4> ------> <stmt-7>
[wp:cil2cfg] get_node: <stmt-3> --> id:1,3
[wp:cil2cfg] add node : <stmt-3>
[wp:cil2cfg] add edge : <stmt-3> ------> <stmt-4>
[wp:cil2cfg] get_node: <stmt-2> --> id:1,2
[wp:cil2cfg] add node : <stmt-2>
[wp:cil2cfg] add edge : <stmt-2> ------> <stmt-3>
[wp:cil2cfg] add edge : <blkIn-fct> ------> <stmt-2>
[wp:cil2cfg] add edge : <fctIn> ------> <blkIn-fct>
[wp:cil2cfg] for function 'swap': 11 vertex - 11 edges
[wp:cil2cfg] start removing unreachable in swap
[wp:cil2cfg] remove unreachable node <exit>
[wp:cil2cfg] for function 'swap': 10 vertex - 10 edges
[wp:cil2cfg] start loop analysis for swap
[wp:cil2cfg] unstructuredness coef = 1.000000
[wp:cil2cfg] done for swap
[wp:annot] collecting unreachable annotations
[wp:annot] process annotations of unreachable node <exit>
[wp:annot] found 0 unreachable annotations
[wp:annot] [get_strategies] 1 behaviors
[wp:annot] build strategy for 'swap', behavior 'default!', all
properties, both assigns or not
[wp:annot] get_node_annot for node <start>
[wp:annot] get_node_annot for node <blkIn-fct>
[wp:annot] get_node_annot for node <blkOut-fct>
[wp:annot] get_node_annot for node <end>
[wp:annot] get_node_annot for node <stmt-4>
[wp:annot] get_node_annot for node <fctIn>
[wp:strategy] 'swap' is NOT the main entry point
[wp:strategy] take (pre_3: (\valid(\at(a,Pre)) ??? \valid(\at(b,Pre))))
[wp:annot] get_node_annot for node <fctOut>
[wp:annot] [goal_to_select] all vs post_1_A -> select (selected)
[wp:strategy] take (post_1_A: (A: *\at(a,Pre) ??? \at(*b,Pre)))
[wp:annot] [goal_to_select] all vs post_2_B -> select (selected)
[wp:strategy] take (post_2_B: (B: *\at(b,Pre) ??? \at(*a,Pre)))
[wp:annot] [goal_to_select] all vs function_assigns -> select (selected)
[wp:strategy] take function_assigns  *a, *b;
[wp:annot] get_node_annot for node <stmt-2>
[wp:annot] get_node_annot for node <stmt-3>
[wp:annot] get_node_annot for node <stmt-7>
[wp] warning: Missing RTE guards
[wp:calculus] [wp-cfg] start computing with the strategy for 'swap',
behavior 'default!', all properties, both assigns or not
[wp:cil2cfg] 0/0 strange loops
[wp:calculus] start computing (pass 1)
[wp:calculus] [wp-cfg] start Pass1
[wp:calculus] [get_wp_edge] get wp before <fctIn>
[wp:calculus] [compute_edge] before <fctIn> go...
[wp:calculus] [get_wp_edge] get wp before <blkIn-fct>
[wp:calculus] [compute_edge] before <blkIn-fct> go...
[wp:calculus] [get_wp_edge] get wp before <stmt-2>
[wp:calculus] [compute_edge] before <stmt-2> go...
[wp:calculus] [get_wp_edge] get wp before <stmt-3>
[wp:calculus] [compute_edge] before <stmt-3> go...
[wp:calculus] [get_wp_edge] get wp before <stmt-4>
[wp:calculus] [compute_edge] before <stmt-4> go...
[wp:calculus] [get_wp_edge] get wp before <stmt-7>
[wp:calculus] [compute_edge] before <stmt-7> go...
[wp:calculus] [get_wp_edge] get wp before <blkOut-fct>
[wp:calculus] [compute_edge] before <blkOut-fct> go...
[wp:calculus] [get_wp_edge] get wp before <fctOut>
[wp:calculus] [compute_edge] before <fctOut> go...
[wp:calculus] [get_wp_edge] get wp before <end>
[wp:calculus] [compute_edge] before <end> go...
[wp:calculus] [compute_edge] before <end> done
[wp:calculus] get proof obligation at edge <fctOut> ------> <end>
[wp:calculus] add goal (post_2_B: (B: *\at(b,Pre) ??? \at(*a,Pre)))
[wp:context] PUSH 0: "add_goal"
[wp:var_analysis] [COMPUTE] DO address taken table computing
[wp:var_analysis] [LP+AT] logic parameters and address taken computation
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b not yet recorded
[wp:funvar] [pointed_of_arity] int *,0
[wp:funvar] [get_funvar] (b,0,false,obj-pointer)
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a not yet recorded
[wp:funvar] [pointed_of_arity] int *,0
[wp:funvar] [get_funvar] (a,0,false,obj-pointer)
[wp:context] POPK 0: "add_goal"
[wp:calculus] add goal (post_1_A: (A: *\at(a,Pre) ??? \at(*b,Pre)))
[wp:context] PUSH 0: "add_goal"
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a already recorded
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b already recorded
[wp:context] POPK 0: "add_goal"
[wp:calculus] add assign goal (function_assigns)
[wp:context] PUSH 0: "add_assigns"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b already recorded
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a already recorded
[wp:funvar] massigned case loc : a
[wp:funvar] [mloc_of_loc] already a loc a
[wp:funvar] massigned case loc : b
[wp:funvar] [mloc_of_loc] already a loc b
[wp:context] POPK 0: "add_assigns"
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <fctOut> ------> <end>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b]))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a]))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1)))
[wp:calculus] [wp_scope] function out : a, b
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:calculus] [compute_edge] before <fctOut> done
[wp:calculus] get proof obligation at edge <blkOut-fct> ------> <fctOut>
[wp:calculus] get proof obligation at label \post
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [do_label] process \post
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <blkOut-fct> ------> <fctOut>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b]))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a]))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1)))
[wp:calculus] [wp_scope] block out : tmp
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:calculus] [compute_edge] before <blkOut-fct> done
[wp:calculus] get proof obligation at edge <stmt-7> ------> <blkOut-fct>
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <stmt-7> ------> <blkOut-fct>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b]))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a]))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1)))
[wp:context] PUSH 0: "return"
[wp:context] POPK 0: "return"
[wp:context] PUSH 0: "return"
[wp:context] POPK 0: "return"
[wp:context] PUSH 0: "return"
[wp:context] POPK 0: "return"
[wp:calculus] [compute_edge] before <stmt-7> done
[wp:calculus] get proof obligation at edge <stmt-4> ------> <stmt-7>
[wp:calculus] get proof obligation at label Stmt sid:7
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [do_label] process Stmt sid:7
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <stmt-4> ------> <stmt-7>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b]))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a]))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1)))
[wp:context] PUSH 0: "assign"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b not yet recorded
[wp:funvar] [pointed_of_arity] int *,0
[wp:funvar] [get_funvar] (b_0,0,false,obj-pointer)
[wp:var_kind] tmp is a funvar
[wp:funvar] [get_funvar] tmp not yet recorded
[wp:funvar] [pointed_of_arity] int,0
[wp:funvar] [get_funvar] (tmp,0,false,sint32)
[wp:context] POPK 0: "assign"
[wp:context] PUSH 0: "assign"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:var_kind] tmp is a funvar
[wp:funvar] [get_funvar] tmp as tmp already recorded
[wp:context] POPK 0: "assign"
[wp:context] PUSH 0: "assign"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:var_kind] tmp is a funvar
[wp:funvar] [get_funvar] tmp as tmp already recorded
[wp:funvar] massigned case loc : b_0
[wp:funvar] [mloc_of_loc] already a loc b_0
[wp:context] POPK 0: "assign"
[wp:calculus] [compute_edge] before <stmt-4> done
[wp:calculus] get proof obligation at edge <stmt-3> ------> <stmt-4>
[wp:calculus] get proof obligation at label Stmt sid:4
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [do_label] process Stmt sid:4
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <stmt-3> ------> <stmt-4>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        (let m_0 = m_0[b_0->data_of_sint32(tmp)] in
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b])))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   (let m_0 = m_0[b_0->data_of_sint32(tmp)] in
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a])))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1))))
[wp:context] PUSH 0: "assign"
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a not yet recorded
[wp:funvar] [pointed_of_arity] int *,0
[wp:funvar] [get_funvar] (a_0,0,false,obj-pointer)
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:context] POPK 0: "assign"
[wp:context] PUSH 0: "assign"
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:context] POPK 0: "assign"
[wp:context] PUSH 0: "assign"
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:funvar] massigned case loc : a_0
[wp:funvar] [mloc_of_loc] already a loc a_0
[wp:context] POPK 0: "assign"
[wp:calculus] [compute_edge] before <stmt-3> done
[wp:calculus] get proof obligation at edge <stmt-2> ------> <stmt-3>
[wp:calculus] get proof obligation at label Stmt sid:3
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [do_label] process Stmt sid:3
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <stmt-2> ------> <stmt-3>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        (let m_0 = m_0[a_0->m_0[b_0]] in
[wp:calculus]        (let m_0 = m_0[b_0->data_of_sint32(tmp)] in
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b]))))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   (let m_0 = m_0[a_0->m_0[b_0]] in
[wp:calculus]   (let m_0 = m_0[b_0->data_of_sint32(tmp)] in
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a]))))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   (let ze = zunion(ze,zrange_of_addr_range(a_0,0,1)) in
[wp:calculus]   (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1)))))
[wp:context] PUSH 0: "assign"
[wp:var_kind] tmp is a funvar
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:funvar] [get_funvar] tmp as tmp already recorded
[wp:context] POPK 0: "assign"
[wp:context] PUSH 0: "assign"
[wp:var_kind] tmp is a funvar
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:funvar] [get_funvar] tmp as tmp already recorded
[wp:context] POPK 0: "assign"
[wp:context] PUSH 0: "assign"
[wp:var_kind] tmp is a funvar
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:funvar] [get_funvar] tmp as tmp already recorded
[wp:funvar] massigned case loc : PATH:tmp of 0
[wp:funvar] [mloc_of_path] PATH:tmp of 0
[wp:funvar] [mcvar] of tmp
[wp:funvar] [mcvar] case of mem
[wp:logic] Adding declaration X_tmp (Local 'tmp')
[wp:context] POPK 0: "assign"
[wp:calculus] [compute_edge] before <stmt-2> done
[wp:calculus] get proof obligation at edge <blkIn-fct> ------> <stmt-2>
[wp:calculus] get proof obligation at label Stmt sid:2
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [do_label] process Stmt sid:2
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <blkIn-fct> ------> <stmt-2>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]      Goal :
[wp:calculus]        (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]        (let m_0 = m_0[a_0->m_0[b_0]] in
[wp:calculus]        (let m_0 = m_0[b_0->data_of_sint32(tmp)] in
[wp:calculus]        tag_A: (sint32_of_data(m_0[a]) = sint32_of_data(m[b])))))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus] Goal :
[wp:calculus]   (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]   (let m_0 = m_0[a_0->m_0[b_0]] in
[wp:calculus]   (let m_0 = m_0[b_0->data_of_sint32(tmp)] in
[wp:calculus]   tag_B: (sint32_of_data(m_0[b]) = sint32_of_data(m[a])))))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus] Goal :
[wp:calculus]   (let ze = zunion(ze,zrange(X_tmp,0,1)) in
[wp:calculus]   (let ze = zunion(ze,zrange_of_addr_range(a_0,0,1)) in
[wp:calculus]   (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]   included(ze,
[wp:calculus]
zunion(zunion(zx,zrange_of_addr_range(a,0,1)),zrange_of_addr_range(b,0,1))))))
[wp:calculus] [wp_scope] block in : tmp
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:var_kind] tmp is a funvar
[wp:funvar] massigned case loc : PATH:tmp of 0
[wp:funvar] [mloc_of_path] PATH:tmp of 0
[wp:funvar] [mcvar] of tmp
[wp:funvar] [mcvar] case of mem
[wp:context] POPK 0: "scope"
[wp:calculus] [wp_scope] function frame : a, b
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:var_kind] a is a funvar
[wp:funvar] massigned case loc : PATH:a of 0
[wp:funvar] [mloc_of_path] PATH:a of 0
[wp:funvar] [mcvar] of a
[wp:funvar] [mcvar] case of mem
[wp:logic] Adding declaration X_a (Local 'a')
[wp:var_kind] b is a funvar
[wp:funvar] massigned case loc : PATH:b of 0
[wp:funvar] [mloc_of_path] PATH:b of 0
[wp:funvar] [mcvar] of b
[wp:funvar] [mcvar] case of mem
[wp:logic] Adding declaration X_b (Local 'b')
[wp:context] POPK 0: "scope"
[wp:calculus] [compute_edge] before <blkIn-fct> done
[wp:calculus] get proof obligation at edge <fctIn> ------> <blkIn-fct>
[wp:calculus] get proof obligation at label \pre
[wp:calculus] add hyp (pre_3: (\valid(\at(a,Pre)) ??? \valid(\at(b,Pre))))
[wp:context] PUSH 0: "add_hyp"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b already recorded
[wp:funvar] massigned case loc : b
[wp:funvar] [mloc_of_loc] already a loc b
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a already recorded
[wp:funvar] massigned case loc : a
[wp:funvar] [mloc_of_loc] already a loc a
[wp:context] POPK 0: "add_hyp"
[wp:context] PUSH 0: "add_hyp"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b already recorded
[wp:funvar] massigned case loc : b
[wp:funvar] [mloc_of_loc] already a loc b
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a already recorded
[wp:funvar] massigned case loc : a
[wp:funvar] [mloc_of_loc] already a loc a
[wp:context] POPK 0: "add_hyp"
[wp:context] PUSH 0: "add_hyp"
[wp:var_kind] b is a funvar
[wp:funvar] [get_funvar] b as b already recorded
[wp:funvar] massigned case loc : b
[wp:funvar] [mloc_of_loc] already a loc b
[wp:var_kind] a is a funvar
[wp:funvar] [get_funvar] a as a already recorded
[wp:funvar] massigned case loc : a
[wp:funvar] [mloc_of_loc] already a loc a
[wp:context] POPK 0: "add_hyp"
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [do_label] process \pre
[wp:context] PUSH 0: "label"
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:funvar] [get_funvar] a as a_0 already recorded
[wp:funvar] [get_funvar] b as b_0 already recorded
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <fctIn> ------> <blkIn-fct>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]       - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]    (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]    (let m_1 = m_0[a_0->m_0[b_0]] in
[wp:calculus]    (let m_2 = m_1[b_0->data_of_sint32(tmp)] in
[wp:calculus]    tag_A: (sint32_of_data(m_2[a_0]) =
sint32_of_data(m_0[b_0]))))))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]    (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]    (let m_3 = m_0[a_0->m_0[b_0]] in
[wp:calculus]    (let m_4 = m_3[b_0->data_of_sint32(tmp)] in
[wp:calculus]    tag_B: (sint32_of_data(m_4[b_0]) =
sint32_of_data(m_0[a_0]))))))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]    (let zx =
zunion(zunion(zempty,zrange(X_a,0,1)),zrange(X_b,0,1)) in
[wp:calculus]    (let zx = zunion(zx,zrange(X_tmp,0,1)) in
[wp:calculus]    (let ze = zunion(zempty,zrange(X_tmp,0,1)) in
[wp:calculus]    (let ze = zunion(ze,zrange_of_addr_range(a_0,0,1)) in
[wp:calculus]    (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]    included(ze,
[wp:calculus]    zunion(zunion(zx,zrange_of_addr_range(a_0,0,1)),
[wp:calculus]      zrange_of_addr_range(b_0,0,1)))))))))
[wp:calculus] [wp_scope] function in : a, b
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:calculus] [wp_scope] global :
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:context] PUSH 0: "scope"
[wp:context] POPK 0: "scope"
[wp:calculus] [compute_edge] before <fctIn> done
[wp:calculus] get proof obligation at edge <start> ------> <fctIn>
[wp:calculus] [do_label] process \here
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:context] PUSH 0: "label"
[wp:context] POPK 0: "label"
[wp:calculus] [set_wp_edge] <start> ------> <fctIn>
[wp:calculus] =   Proof Obligation post_1_A:
[wp:calculus]       - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]     (let m_1 = m_0[a_0->m_0[b_0]] in
[wp:calculus]     (let m_2 = m_1[b_0->data_of_sint32(tmp)] in
[wp:calculus]     tag_A: (sint32_of_data(m_2[a_0]) =
sint32_of_data(m_0[b_0])))))))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]     (let m_3 = m_0[a_0->m_0[b_0]] in
[wp:calculus]     (let m_4 = m_3[b_0->data_of_sint32(tmp)] in
[wp:calculus]     tag_B: (sint32_of_data(m_4[b_0]) =
sint32_of_data(m_0[a_0])))))))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let zx =
zunion(zunion(zempty,zrange(X_a,0,1)),zrange(X_b,0,1)) in
[wp:calculus]     (let zx = zunion(zx,zrange(X_tmp,0,1)) in
[wp:calculus]     (let ze = zunion(zempty,zrange(X_tmp,0,1)) in
[wp:calculus]     (let ze = zunion(ze,zrange_of_addr_range(a_0,0,1)) in
[wp:calculus]     (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]     included(ze,
[wp:calculus]     zunion(zunion(zx,zrange_of_addr_range(a_0,0,1)),
[wp:calculus]       zrange_of_addr_range(b_0,0,1))))))))))
[wp:calculus] [get_wp_edge] get wp before <stmt-2>
[wp:calculus] [get_wp_edge] <stmt-2> already computed
[wp:calculus] [get_wp_edge] get wp before <fctOut>
[wp:calculus] [get_wp_edge] <fctOut> already computed
[wp:calculus] [get_wp_edge] get wp before <stmt-7>
[wp:calculus] [get_wp_edge] <stmt-7> already computed
[wp:calculus] [get_wp_edge] get wp before <blkIn-fct>
[wp:calculus] [get_wp_edge] <blkIn-fct> already computed
[wp:calculus] [get_wp_edge] get wp before <end>
[wp:calculus] [get_wp_edge] <end> already computed
[wp:calculus] [get_wp_edge] get wp before <stmt-3>
[wp:calculus] [get_wp_edge] <stmt-3> already computed
[wp:calculus] [get_wp_edge] get wp before <stmt-4>
[wp:calculus] [get_wp_edge] <stmt-4> already computed
[wp:calculus] [get_wp_edge] get wp before <blkOut-fct>
[wp:calculus] [get_wp_edge] <blkOut-fct> already computed
[wp:calculus] [wp-cfg] end of Pass1
[wp:calculus] [get_wp_edge] get wp before <fctIn>
[wp:calculus] [get_wp_edge] <fctIn> already computed
[wp:strategy] 'swap' is NOT the main entry point
[wp:calculus] before close: Proof Obligation post_1_A:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]     (let m_1 = m_0[a_0->m_0[b_0]] in
[wp:calculus]     (let m_2 = m_1[b_0->data_of_sint32(tmp)] in
[wp:calculus]     tag_A: (sint32_of_data(m_2[a_0]) =
sint32_of_data(m_0[b_0])))))))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]     (let m_3 = m_0[a_0->m_0[b_0]] in
[wp:calculus]     (let m_4 = m_3[b_0->data_of_sint32(tmp)] in
[wp:calculus]     tag_B: (sint32_of_data(m_4[b_0]) =
sint32_of_data(m_0[a_0])))))))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let zx =
zunion(zunion(zempty,zrange(X_a,0,1)),zrange(X_b,0,1)) in
[wp:calculus]     (let zx = zunion(zx,zrange(X_tmp,0,1)) in
[wp:calculus]     (let ze = zunion(zempty,zrange(X_tmp,0,1)) in
[wp:calculus]     (let ze = zunion(ze,zrange_of_addr_range(a_0,0,1)) in
[wp:calculus]     (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]     included(ze,
[wp:calculus]     zunion(zunion(zx,zrange_of_addr_range(a_0,0,1)),
[wp:calculus]       zrange_of_addr_range(b_0,0,1))))))))))
[wp:context] PUSH 0: "close"
[wp:context] FLUSH 0 "close"
[wp:context] PUSH 0: "close"
[wp:context] FLUSH 0 "close"
[wp:context] PUSH 0: "close"
[wp:context] FLUSH 0 "close"
[wp:calculus] [get_weakest_precondition] Proof Obligation post_1_A:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (forall b_0:pointer.
[wp:calculus]   (forall a_0:pointer.
[wp:calculus]   (forall m_0:data farray.
[wp:calculus]   (forall ta_0:int farray.
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]     (let m_1 = m_0[a_0->m_0[b_0]] in
[wp:calculus]     (let m_2 = m_1[b_0->data_of_sint32(tmp)] in
[wp:calculus]     tag_A: (sint32_of_data(m_2[a_0]) =
sint32_of_data(m_0[b_0])))))))))))
[wp:calculus]
[wp:calculus] Proof Obligation post_2_B:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (forall b_0:pointer.
[wp:calculus]   (forall a_0:pointer.
[wp:calculus]   (forall m_0:data farray.
[wp:calculus]   (forall ta_0:int farray.
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let tmp = sint32_of_data(m_0[a_0]) in
[wp:calculus]     (let m_3 = m_0[a_0->m_0[b_0]] in
[wp:calculus]     (let m_4 = m_3[b_0->data_of_sint32(tmp)] in
[wp:calculus]     tag_B: (sint32_of_data(m_4[b_0]) =
sint32_of_data(m_0[a_0])))))))))))
[wp:calculus]
[wp:calculus] Proof Obligation function_assigns:
[wp:calculus]  - Assumes Pre-condition (file wp.c, line 1) in 'swap'
[wp:calculus] Goal :
[wp:calculus]   (forall b_0:pointer.
[wp:calculus]   (forall a_0:pointer.
[wp:calculus]   (forall ta_0:int farray.
[wp:calculus]   (global(ta_0) ->
[wp:calculus]    ((valid(ta_0,a_0,1) and valid(ta_0,b_0,1)) ->
[wp:calculus]     (let zx =
zunion(zunion(zempty,zrange(X_a,0,1)),zrange(X_b,0,1)) in
[wp:calculus]     (let zx = zunion(zx,zrange(X_tmp,0,1)) in
[wp:calculus]     (let ze = zunion(zempty,zrange(X_tmp,0,1)) in
[wp:calculus]     (let ze = zunion(ze,zrange_of_addr_range(a_0,0,1)) in
[wp:calculus]     (let ze = zunion(ze,zrange_of_addr_range(b_0,0,1)) in
[wp:calculus]     included(ze,
[wp:calculus]     zunion(zunion(zx,zrange_of_addr_range(a_0,0,1)),
[wp:calculus]       zrange_of_addr_range(b_0,0,1)))))))))))))
[wp:calculus] [wp-cfg] computing done.
[wp:cfgproof] Export PO post_1_A
[wp:cfgproof] DO HEADER in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_1_A_head.txt
[wp:cfgproof] DONE HEADER in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_1_A_head.txt
[wp:cfgproof] DO BODY in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_1_A_body.txt
[wp:cfgproof] DONE BODY in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_1_A_body.txt
[wp:cfgproof] Into gui config, goal has to be produce in all languages
[wp:cfgproof] DO export goal in language Why
[wp:cfgproof] DONE export goal in language Why
[wp:cfgproof] DO export goal in language Coq
[wp:cfgproof] DONE export goal in language Coq
[wp:cfgproof] DO export goal in language Alt-Ergo
[wp:cfgproof] DONE export goal in language Alt-Ergo
[wp:cfgproof] Export PO post_2_B
[wp:cfgproof] DO HEADER in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_2_B_head.txt
[wp:cfgproof] DONE HEADER in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_2_B_head.txt
[wp:cfgproof] DO BODY in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_2_B_body.txt
[wp:cfgproof] DONE BODY in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_post_2_B_body.txt
[wp:cfgproof] Into gui config, goal has to be produce in all languages
[wp:cfgproof] DO export goal in language Why
[wp:cfgproof] DONE export goal in language Why
[wp:cfgproof] DO export goal in language Coq
[wp:cfgproof] DONE export goal in language Coq
[wp:cfgproof] DO export goal in language Alt-Ergo
[wp:cfgproof] DONE export goal in language Alt-Ergo
[wp:cfgproof] Export PO function_assigns
[wp:cfgproof] DO HEADER in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_function_assigns_head.txt
[wp:cfgproof] DONE HEADER in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_function_assigns_head.txt
[wp:cfgproof] DO BODY in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_function_assigns_body.txt
[wp:cfgproof] DONE BODY in
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_swap_function_assigns_body.txt
[wp:cfgproof] Into gui config, goal has to be produce in all languages
[wp:cfgproof] DO export goal in language Why
[wp:cfgproof] DONE export goal in language Why
[wp:cfgproof] DO export goal in language Coq
[wp:cfgproof] DONE export goal in language Coq
[wp:cfgproof] DO export goal in language Alt-Ergo
[wp:cfgproof] DONE export goal in language Alt-Ergo
[wp] [WP:simplified] Goal store_swap_function_assigns : Valid
[wp:cfgproof] DO ENV DESCP
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_env1.txt
[wp:cfgproof] DONE ENV DESCP
C:/DOKUME~1/sylvain/LOKALE~1/Temp\wp68d0ad.dir/store_env1.txt
[wp:cfgproof] DO export env for Why
[wp:cfgproof] DO export env for Coq
[wp:cfgproof] DO export env for Alt-Ergo