Skip to content
Snippets Groups Projects
Commit 451eb059 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] changed order of declarations

parent c98c5436
No related branches found
No related tags found
No related merge requests found
......@@ -22,9 +22,9 @@ theory Compound
(* use frama_c_wp.memory.Memory *)
function shift_sint32 (p:addr) (k:int) : addr = shift p k
function shiftfield_F1__list_next (p:addr) : addr = shift p 1
function shift_sint32 (p:addr) (k:int) : addr = shift p k
end
[wp:print-generated]
theory WP
......
......@@ -28,9 +28,9 @@
Require Import Qed.
Require Import Memory.
Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z).
Definition shiftfield_F1__list_next (p : addr) : addr := (shift p 1%Z).
Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z).
[wp:print-generated]
"WPOUT/typed/lemma_test_Coq.v"
(* ---------------------------------------------------------- *)
......
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