generated_proof_int_ptr3.v 900 Bytes
Newer Older
1
2
3
4
5
6
From refinedc.typing Require Import typing.
From refinedc.examples.intptr Require Import generated_code.
From refinedc.examples.intptr Require Import generated_spec.
Set Default Proof Using "Type".

(* Generated from [examples/intptr.c]. *)
7
Section proof_int_ptr3.
8
9
  Context `{!typeG Σ} `{!globalG Σ}.

10
11
12
  (* Typing proof for [int_ptr3]. *)
  Lemma type_int_ptr3 :
     typed_function impl_int_ptr3 type_of_int_ptr3.
13
  Proof.
14
    Open Scope printing_sugar.
15
    start_function "int_ptr3" (l) => arg_p local_i.
16
17
18
19
20
21
    split_blocks ((
      
    )%I : gmap label (iProp Σ)) ((
      
    )%I : gmap label (iProp Σ)).
    - repeat liRStep; liShow.
22
      all: print_typesystem_goal "int_ptr3" "#0".
23
    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
24
    all: print_sidecondition_goal "int_ptr3".
25
  Qed.
26
End proof_int_ptr3.