Fix proofs and example programs

.gitignore

@@ -16,3 +16,4 @@ examples/authproxy
 examples/gnatprove
 undefined.ciu
 graph.vcg
+*.ci

Makefile

@@ -5,9 +5,7 @@ EXAMPLES = b64 json area jwt authproxy
 CALLGRAPH = none
 
 all: JWX.gpr
-	@time gnatprove $(COMMON_OPTS) -PJWX $(GNATPROVE_OPTS) | tee proof.log.tmp
-	@egrep -v -q '\(medium\|warning\|error\):' proof.log.tmp
-	@mv proof.log.tmp proof.log
+	@gnatprove $(COMMON_OPTS) -PJWX $(GNATPROVE_OPTS)
 
 clean: JWX.gpr
 	@make -C contrib/libsparkcrypto clean
@@ -36,7 +34,7 @@ examples:: $(addprefix obj/,$(EXAMPLES))
 
 $(addprefix obj/,$(EXAMPLES)): obj/lsc/libsparkcrypto.gpr examples/*.ad?
 	@gprbuild $(COMMON_OPTS) -P examples/examples.gpr
-	@gnatprove $(COMMON_OPTS) -P examples/examples.gpr $(GNATPROVE_OPTS)
+	@gnatprove $(COMMON_OPTS) -P examples/examples.gpr
 
 JWX.gpr: obj/lsc/libsparkcrypto.gpr
 

examples/authproxy.adb

@@ -248,6 +248,7 @@ begin
    Create_Socket (Socket => Server_Socket);
    Set_Socket_Option
       (Socket => Server_Socket,
+       Level  => Socket_Level,
        Option => (Name => Reuse_Address, Enabled => True));
    Bind_Socket
       (Socket  => Server_Socket,

examples/examples.gpr

@@ -14,4 +14,17 @@ project Examples is
       for Switches use ("-a", "-p");
    end Stack;
 
+   package Prove is
+      for Proof_Switches ("Ada") use
+      (
+         "-j0",
+         "--prover=z3,cvc4,altergo",
+         "--steps=1000",
+         "--timeout=60",
+         "--memlimit=1000",
+         "--checks-as-errors",
+         "--warnings=error"
+      );
+   end Prove;
+
 end Examples;