(* Do not edit this file, it was generated automatically *)
Require Import VST.floyd.proofauto.
Require Import VST.concurrency.conclib.
Require Import VST.concurrency.ghosts.
From VSTlib Require Import spec_locks spec_threads spec_malloc.
Require VSTlib.verif_locks.
Require Import VSTlibtest.incr_main.
Require Import VSTlibtest.verif_incr.
Require Import VST.floyd.VSU.

Require VSTlib.verif_threads.
Definition AB_VSU :=
  ltac:(linkVSUs (verif_SC_atomics.SCAVSU) (verif_threads.ThreadsVSU)).

Require VSTlib.verif_locks.
Definition ABC_VSU :=
  ltac:(linkVSUs AB_VSU verif_locks.LockVSU).

Ltac SC_tac ::=
 match goal with |- SC_test ?ids _ _ =>
  let a := eval compute in ids in change ids with a
 end;
 hnf;
 repeat (apply conj; hnf);
 lazymatch goal with
         | |- Funspecs_must_match ?i _ _ =>
                 try solve [constructor; unfold abbreviate; 
                 try simple apply eq_refl;  (* This line needs to be added to floyd/VSU.v *)
                 repeat f_equal]
         | |- Identifier_not_found ?i ?fds2 =>
                 fail "identifer" i "not found in funspecs" fds2
         | |- True => trivial
          end.

Definition core_VSU :=
  ltac:(linkVSUs IncrVSU ABC_VSU).

#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition main_QPprog := ltac:(QPprog prog).
Definition whole_prog := ltac:(QPlink_progs main_QPprog (VSU_prog core_VSU)).
Definition Vprog: varspecs := QPvarspecs whole_prog.
Definition Main_imports := filter (matchImportExport main_QPprog) (VSU_Exports core_VSU). 

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE  [] main_pre whole_prog tt gv
  POST [ tint ] PROP() RETURN (Vint (Int.repr 2)) SEP (TT).

Definition Gprog :=  [main_spec] ++ Main_imports.

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
pose core_VSU.
  start_function.
  sep_apply (make_mem_mgr gv).
  forward_call.
 unfold InitGPred; simpl. Intros. unfold globvar2pred; simpl.
 change (Maps.PTree.prev _) with incr._c.
 change 16 with (@sizeof verif_incr.CompSpecs t_counter).
 sep_apply (@mapsto_zero_data_at_zero verif_incr.CompSpecs t_counter Ews (gv incr._c)); 
       auto with field_compatible.
  repeat (rewrite zero_val_eq; simpl).
  repeat change (fold_reptype ?a) with a.
  repeat unfold_data_at (data_at _ _ _ _).
  cancel.
  forward.
Qed.

Definition MainComp:  MainCompType nil main_QPprog core_VSU whole_prog (snd main_spec)  emp.
Proof.
mkComponent prog.
solve_SF_internal body_main.
Qed.

Lemma WholeComp: WholeCompType core_VSU MainComp.
Proof. proveWholeComponent. Qed.

Lemma WholeProgSafe: WholeProgSafeType WholeComp tt.
Proof. proveWholeProgSafe. Qed.

(* Eval red in WholeProgSafeType WholeComp tt. *)


(*

Definition extlink := ext_link_prog prog. (* this is wrong, because
       it doesn't include the programs of all the imported VSUs *)
Definition Espec := add_funspecs (Concurrent_Espec unit _ extlink) extlink Gprog.
*)
