Commit a1d0aaf4 authored by Michael Sammler's avatar Michael Sammler
Browse files

remove sketches from ocaml runtime code

parent 0c5a0fca
Pipeline #49833 passed with stage
in 22 minutes and 11 seconds
......@@ -18,23 +18,6 @@ typedef uintnat value;
#define Is_long(x) (((x) & 1) != 0)
#define Is_block(x) (((x) & 1) == 0)
//@rc::inlined
//@ Definition ocaml_value (b:bool) : type :=
//@ tyexists (λ p, b @ optional (p.1 @ intptr i64) (p.2 @ int i64))%I.
//@ Global Program Instance optionable_intptr_int l i it :
//@ Optionable (l @ intptr it) (i @ int it) (IntOp it) (IntOp it) := {|
//@ opt_pre _ _ := False%I;
//@ |}.
//@ Next Obligation. done. Qed.
//@ Next Obligation. iIntros (????????? ?). done. Qed.
//@rc::end
/* [[rc::parameters("b : bool")]] */
/* [[rc::args("ocaml_value<b>")]] */
/* [[rc::returns("b @ boolean<bool_it>")]] */
/* bool Is_long(value x) { return (((x) & 1) != 0); } */
/* bool Is_block(value x) { return (((x) & 1) == 0); } */
// Conversion from/to a Long (name format used everywhere: "to_from").
/* #define Val_long(x) ((intnat) (((uintnat)(x) << 1)) + 1) */
#define Val_long(x) ((value) (((uintnat)(x) << 1)) + 1)
......
......@@ -6,55 +6,55 @@ Set Default Proof Using "Type".
(* Generated from [examples/ocaml_runtime.c]. *)
Section code.
Definition file_0 : string := "examples/ocaml_runtime.c".
Definition loc_2 : location_info := LocationInfo file_0 46 2 46 39.
Definition loc_3 : location_info := LocationInfo file_0 47 2 47 30.
Definition loc_4 : location_info := LocationInfo file_0 49 2 49 32.
Definition loc_5 : location_info := LocationInfo file_0 50 2 50 57.
Definition loc_6 : location_info := LocationInfo file_0 52 2 52 28.
Definition loc_7 : location_info := LocationInfo file_0 53 2 53 28.
Definition loc_8 : location_info := LocationInfo file_0 55 2 55 54.
Definition loc_9 : location_info := LocationInfo file_0 56 2 56 28.
Definition loc_10 : location_info := LocationInfo file_0 57 2 57 39.
Definition loc_11 : location_info := LocationInfo file_0 57 9 57 37.
Definition loc_12 : location_info := LocationInfo file_0 57 9 57 23.
Definition loc_13 : location_info := LocationInfo file_0 57 9 57 23.
Definition loc_14 : location_info := LocationInfo file_0 57 10 57 23.
Definition loc_15 : location_info := LocationInfo file_0 57 10 57 23.
Definition loc_16 : location_info := LocationInfo file_0 57 27 57 37.
Definition loc_17 : location_info := LocationInfo file_0 56 9 56 26.
Definition loc_18 : location_info := LocationInfo file_0 56 9 56 20.
Definition loc_19 : location_info := LocationInfo file_0 56 10 56 14.
Definition loc_20 : location_info := LocationInfo file_0 56 10 56 14.
Definition loc_21 : location_info := LocationInfo file_0 56 18 56 19.
Definition loc_22 : location_info := LocationInfo file_0 56 24 56 26.
Definition loc_23 : location_info := LocationInfo file_0 55 33 55 53.
Definition loc_24 : location_info := LocationInfo file_0 55 51 55 53.
Definition loc_25 : location_info := LocationInfo file_0 55 51 55 53.
Definition loc_28 : location_info := LocationInfo file_0 53 9 53 26.
Definition loc_29 : location_info := LocationInfo file_0 53 10 53 20.
Definition loc_30 : location_info := LocationInfo file_0 53 11 53 15.
Definition loc_31 : location_info := LocationInfo file_0 53 11 53 15.
Definition loc_32 : location_info := LocationInfo file_0 53 18 53 19.
Definition loc_33 : location_info := LocationInfo file_0 53 24 53 25.
Definition loc_34 : location_info := LocationInfo file_0 52 9 52 26.
Definition loc_35 : location_info := LocationInfo file_0 52 10 52 20.
Definition loc_36 : location_info := LocationInfo file_0 52 11 52 15.
Definition loc_37 : location_info := LocationInfo file_0 52 11 52 15.
Definition loc_38 : location_info := LocationInfo file_0 52 18 52 19.
Definition loc_39 : location_info := LocationInfo file_0 52 24 52 25.
Definition loc_40 : location_info := LocationInfo file_0 50 13 50 56.
Definition loc_41 : location_info := LocationInfo file_0 50 14 50 51.
Definition loc_42 : location_info := LocationInfo file_0 50 22 50 51.
Definition loc_43 : location_info := LocationInfo file_0 50 24 50 44.
Definition loc_44 : location_info := LocationInfo file_0 50 33 50 44.
Definition loc_45 : location_info := LocationInfo file_0 50 33 50 44.
Definition loc_46 : location_info := LocationInfo file_0 50 48 50 49.
Definition loc_47 : location_info := LocationInfo file_0 50 54 50 55.
Definition loc_50 : location_info := LocationInfo file_0 49 13 49 31.
Definition loc_51 : location_info := LocationInfo file_0 49 21 49 31.
Definition loc_52 : location_info := LocationInfo file_0 49 22 49 31.
Definition loc_55 : location_info := LocationInfo file_0 47 27 47 29.
Definition loc_58 : location_info := LocationInfo file_0 46 28 46 38.
Definition loc_2 : location_info := LocationInfo file_0 29 2 29 39.
Definition loc_3 : location_info := LocationInfo file_0 30 2 30 30.
Definition loc_4 : location_info := LocationInfo file_0 32 2 32 32.
Definition loc_5 : location_info := LocationInfo file_0 33 2 33 57.
Definition loc_6 : location_info := LocationInfo file_0 35 2 35 28.
Definition loc_7 : location_info := LocationInfo file_0 36 2 36 28.
Definition loc_8 : location_info := LocationInfo file_0 38 2 38 54.
Definition loc_9 : location_info := LocationInfo file_0 39 2 39 28.
Definition loc_10 : location_info := LocationInfo file_0 40 2 40 39.
Definition loc_11 : location_info := LocationInfo file_0 40 9 40 37.
Definition loc_12 : location_info := LocationInfo file_0 40 9 40 23.
Definition loc_13 : location_info := LocationInfo file_0 40 9 40 23.
Definition loc_14 : location_info := LocationInfo file_0 40 10 40 23.
Definition loc_15 : location_info := LocationInfo file_0 40 10 40 23.
Definition loc_16 : location_info := LocationInfo file_0 40 27 40 37.
Definition loc_17 : location_info := LocationInfo file_0 39 9 39 26.
Definition loc_18 : location_info := LocationInfo file_0 39 9 39 20.
Definition loc_19 : location_info := LocationInfo file_0 39 10 39 14.
Definition loc_20 : location_info := LocationInfo file_0 39 10 39 14.
Definition loc_21 : location_info := LocationInfo file_0 39 18 39 19.
Definition loc_22 : location_info := LocationInfo file_0 39 24 39 26.
Definition loc_23 : location_info := LocationInfo file_0 38 33 38 53.
Definition loc_24 : location_info := LocationInfo file_0 38 51 38 53.
Definition loc_25 : location_info := LocationInfo file_0 38 51 38 53.
Definition loc_28 : location_info := LocationInfo file_0 36 9 36 26.
Definition loc_29 : location_info := LocationInfo file_0 36 10 36 20.
Definition loc_30 : location_info := LocationInfo file_0 36 11 36 15.
Definition loc_31 : location_info := LocationInfo file_0 36 11 36 15.
Definition loc_32 : location_info := LocationInfo file_0 36 18 36 19.
Definition loc_33 : location_info := LocationInfo file_0 36 24 36 25.
Definition loc_34 : location_info := LocationInfo file_0 35 9 35 26.
Definition loc_35 : location_info := LocationInfo file_0 35 10 35 20.
Definition loc_36 : location_info := LocationInfo file_0 35 11 35 15.
Definition loc_37 : location_info := LocationInfo file_0 35 11 35 15.
Definition loc_38 : location_info := LocationInfo file_0 35 18 35 19.
Definition loc_39 : location_info := LocationInfo file_0 35 24 35 25.
Definition loc_40 : location_info := LocationInfo file_0 33 13 33 56.
Definition loc_41 : location_info := LocationInfo file_0 33 14 33 51.
Definition loc_42 : location_info := LocationInfo file_0 33 22 33 51.
Definition loc_43 : location_info := LocationInfo file_0 33 24 33 44.
Definition loc_44 : location_info := LocationInfo file_0 33 33 33 44.
Definition loc_45 : location_info := LocationInfo file_0 33 33 33 44.
Definition loc_46 : location_info := LocationInfo file_0 33 48 33 49.
Definition loc_47 : location_info := LocationInfo file_0 33 54 33 55.
Definition loc_50 : location_info := LocationInfo file_0 32 13 32 31.
Definition loc_51 : location_info := LocationInfo file_0 32 21 32 31.
Definition loc_52 : location_info := LocationInfo file_0 32 22 32 31.
Definition loc_55 : location_info := LocationInfo file_0 30 27 30 29.
Definition loc_58 : location_info := LocationInfo file_0 29 28 29 38.
(* Definition of function [client]. *)
Definition impl_client : function := {|
......
......@@ -6,17 +6,6 @@ Set Default Proof Using "Type".
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Inlined code. *)
Definition ocaml_value (b:bool) : type :=
tyexists (λ p, b @ optional (p.1 @ intptr i64) (p.2 @ int i64))%I.
Global Program Instance optionable_intptr_int l i it :
Optionable (l @ intptr it) (i @ int it) (IntOp it) (IntOp it) := {|
opt_pre _ _ := False%I;
|}.
Next Obligation. done. Qed.
Next Obligation. iIntros (????????? ?). done. Qed.
(* Type definitions. *)
(* Specifications for function [client]. *)
......
Supports Markdown
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