"
This is the first example from the paper: 

SAGE: Whitebox Fuzzing for Security Testing by
Patrice Godefroid, Michael Y. Levin, David Molnar

int foo(int x) { // x is an input
  int y = x + 3;
  if (y == 13) abort(); // error
  return 0;
} 

"

"
First note that they are using 32-bit numbers, so we will define the 
appropriate data type.
"

(defdata int32 
  (range integer ((- (expt 2 31)) <= _ < (expt 2 31))))

(definec foo (x :int32) :bool
  (let ((y (+ x 3)))                  
    (if (and (equal y 13)
             (int32p y)) ;; instead of defining int32+
        nil              ;; nil for BOOM! You've been hacked.
      t)))  ;; t for OK 


"
;; The reachability question gets turned into this conjecture, which
;; states that foo is always t, i.e., foo never reaches BOOM.
"

(test? (implies (int32p x)
                (equal (foo x) t)))

" 
Example 2. C# code, but the idea is that there is an error when the
value of cnt is >= 4.

void top (char input[4] {
  int cnt=0;
  if (input[0] == 'b') cnt++;
  if (input[1] == 'a') cnt++;
  if (input[2] == 'd') cnt++;
  if (input[3] == '!') cnt++;
  if (cnt >= 4) abort(); ?? error
}
"

(defdata char4 (list character character character character))
(defdata ret (enum '(error ok)))

"

Here is how we might define a macro to help us translate the above
code in a concise way.

"

(defmacro inc-cnt (i char)
  `(if (equal (nth ,i input) ,char) (1+ cnt) cnt))

:trans1 (inc-cnt 0 #\b)

(definec top (input :char4) :ret
  (let* ((cnt 0)
         (cnt (inc-cnt 0 #\b)) ; expands into:
;;       (cnt (if (equal (nth 0 input) #\b) (1+ cnt) cnt))         
         (cnt (inc-cnt 1 #\a))
         (cnt (inc-cnt 2 #\d))
         (cnt (inc-cnt 3 #\!)))
    (if (>= cnt 4) 'error 'ok)))

(test? (implies (char4p input)
                (not (equal (top input) 'error))))