Library NullExtension

Require Import sepcomp.extspec.
Require Import sepcomp.step_lemmas.
Require Import veric.base.
Require Import veric.Clight_new.
Require Import veric.Clight_lemmas.
Require Import veric.juicy_extspec.
Require Import veric.juicy_mem.

Definition dryspec : external_specification juicy_mem external_function unit
  := Build_external_specification juicy_mem external_function unit
     
     (fun ef => False)
     
     (fun ef Hef tys vl m z => False)
     
     (fun ef Hef ty vl m z => False)
     
     (fun rv m z => False).

Definition Espec : OracleKind.
 refine (Build_OracleKind unit (Build_juicy_ext_spec _ dryspec _ _ _)).
Proof.
simpl; intros; contradiction.
simpl; intros; contradiction.
simpl; intros; intros ? ? ? ?; contradiction.
Defined.