jldodds

Require Import floyd.proofauto

Goal forall a b, is_int I32 Signed a -> is_int I32 Signed b ->
exists i i1, sem_add_default tint tint a b = Some (Vint (Int.add i i1)).
intros. destruct a; try solve [inversion H]. 
destruct b; try solve [inversion H0].
unfold sem_add_default.  simpl. unfold both_int. simpl.
eauto.
Qed.

jldodds

Ltac run_rtac reify term_table tac_sound reduce :=
start_timer "total";
start_timer "02 match_tactic";
  lazymatch type of tac_sound with
    | forall t, @rtac_sound _ _ _ _ _ _ (?tac _) =>
	  let namee := fresh "e" in
	  match goal with
	    | |- ?P => 
              stop_timer "02 match_tactic";
              start_timer "03 reification";

jldodds

#include<stdio.h>

void incptr(int* n){
    *n = *n+1;
}

int* return_out_of_scope(){
    int n=0;
    return &n;
}

jldodds

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Import ListNotations.

Open Scope string_scope.

(* Make it print lists one item per line*)
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))
  (format "[ '[' x ;  '//' y ;  '//' .. ;  '//' z ']' ]") : list_scope.