(*
 * Copyright (C) BedRock Systems Inc. 2019 Gregory Malecha
 *
 * This software is distributed under the terms of the BedRock Open-Source License.
 * See the LICENSE-BedRock file in the repository root for details.
 *)
Require Import bedrock.auto.cpp.specs.
Notation "[∗ list] _ ↦ _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∗ list] _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∧ list] _ ↦ _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∧ list] _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∨ list] _ ↦ _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∨ list] _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∗ map] _ ↦ _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Notation "[∗ map] _ ∈ _ , _" was already used in scope
bi_scope. [notation-overridden,parsing]
Notation "[∗ set] _ ∈ _ , _" was already used in scope
bi_scope. [notation-overridden,parsing]
Notation "[∗ mset] _ ∈ _ , _" was already used in
scope bi_scope. [notation-overridden,parsing]
Require Import bedrock.lib.module.
From bedrock_auto.tests.val_cat Require Import val_cat_cpp val_cat_cpp_names.
Custom entry cppglobal has been overridden.
[custom-entry-overridden,parsing]
Local Open Scope Z_scope.
Import primitives.
Import _'.

Section with_Σ.
  Context `{Σ : cpp_logic} `{MOD : val_cat_cpp.module ⊧ σ}.

  Definition PR_def q (m : Z) : Rep :=
    _field `::P::x` |-> intR q m **
    _paddingR q "_Z1P".
  Definition PR_aux : seal (@PR_def).
thread_info:biIndex
Σ:cpp_logic thread_info
σ:genv
MOD:module ⊧ σ
seal PR_def Proof.
thread_info:biIndex
Σ:cpp_logic thread_info
σ:genv
MOD:module ⊧ σ
seal PR_def by eexists. Qed.
  Definition PR := PR_aux.(unseal).
  Definition PR_eq : @PR = _ := PR_aux.(seal_eq).


  Definition _ZN1PC1Ev_spec := [CHECK]
    SPECIFY (mangled "P::P()") (fun this =>
        \post this |-> PR 1 0
      ).

  Definition _ZN1PC1Ei_spec := [CHECK]
    SPECIFY (mangled "P::P(int)") (fun this =>
        \arg{i} "i" (Vint i)
        \post this |-> PR 1 i
      ).

  Definition _ZN1PC1ERKS__spec := [CHECK]
    SPECIFY (mangled "P::P(const P&)") (fun this =>
        \arg{p} "p" (Vptr p)
        \pre{m q}  p |-> PR q m
        \post p |-> PR q m ** this |-> PR 1 m
      ).

  Definition _ZN1PC1EOKS__spec := [CHECK]
    SPECIFY (mangled "P::P(const P&&)") (fun this =>
        \arg{p} "p" (Vptr p)
        \pre{m q}  p |-> PR q m
        \post Exists m', p |-> PR q m' ** this |-> PR 1 m
      ).

  Definition _ZN1PD0Ev_spec := [CHECK]
    SPECIFY (mangled "P::~P()") (fun this =>
        \pre  this |-> anyR (Tnamed "_Z1P") 1
        \post emp
      ).

  Definition _Z6by_refR1P_spec := [CHECK]
    SPECIFY (mangled "by_ref(P&)")
      (\arg{x} "x" (Vptr x)
       \pre{q m}     x |-> PR q m
       \post[Vint m] x |-> PR q m
      ).

  Definition _Z6by_val1P_spec := [CHECK]
    SPECIFY (mangled "by_val(P)")
      (\arg{x} "x" (Vptr x)
       \pre{m}       x |-> PR 1 m
       \post[Vint m] x |-> PR 1 m
      ).

  Definition _Z6by_ptrP1P_spec := [CHECK]
    SPECIFY (mangled "by_ptr(P*)")
      (\arg{x} "x" (Vptr x)
       \pre{q m}            x |-> PR q m
       \post[Vint m] x |-> PR q m
      ).

  Definition _Z7by_rrefO1P_spec := [CHECK]
    SPECIFY (mangled "by_rref(P&&)")
      (\arg{x} "x" (Vptr x)
       \pre{q m}            x |-> PR q m
       \post[Vint m] x |-> PR q m
      ).

  Definition _Z7ret_valv_spec := [CHECK]
    SPECIFY (mangled "ret_val()")
      (\post{r}[Vptr r] r |-> PR 1 1
      ).

  Definition _Z7ret_refR1P_spec := [CHECK]
    SPECIFY (mangled "ret_ref(P&)")
      (\arg{x} "x" (Vptr x)
       \pre{q m}     x |-> PR q m
       \post[Vptr x] x |-> PR q m
      ).

  Definition _Z8ret_rrefR1P_spec := [CHECK]
    SPECIFY (mangled "ret_rref(P&)")
      (\with m q
       \arg{x} "x" (Vptr x)
       \pre            x |-> PR q m
       \post[Vptr x] x |-> PR q m
      ).

  Definition _Z4main_spec := [CHECK]
    SPECIFY (exact "main")
      (\pre  emp
       \post[Vint 0] emp
      ).

  Definition internal_spec : mpred :=
    _ZN1PC1Ev_spec **
    _ZN1PC1Ei_spec **
    _ZN1PC1ERKS__spec **
    _ZN1PC1EOKS__spec **
    _ZN1PD0Ev_spec **
    _Z6by_refR1P_spec **
    _Z6by_val1P_spec **
    _Z6by_ptrP1P_spec **
    _Z7by_rrefO1P_spec **
    _Z7ret_valv_spec **
    _Z7ret_refR1P_spec **
    _Z8ret_rrefR1P_spec.

  Definition public_spec : mpred :=
    wp_mfptr emp _Z4main_spec.

End with_Σ.