Changes between Version 6 and Version 7 of Challenge

Timestamp:

03/12/19 03:45:38 (7 years ago)

Author:

siegel

Comment:

--

Challenge

@@ -7 +7 @@
   `printf`, `assert`, `malloc`, `free`, ....
 Be sure to include the appropriate headers.
+
+ `$input decl`::
+ Declares a variable in file scope to be an input variable.  An input variable
+ `X` is initialized according to the following protocol: (1) if a value for `X`
+ is specified on the command line via `-inputX=val`, then `val` is the
+ initial value; (2) otherwise, if an initializer is present in the declaration, the
+ initializer is used; (3) otherwise, `X` is assigned an unconstrained value
+ of its type---when using symbolic execution, it is assigned a fresh symbolic
+ constant.
 
  `$when (expr) stmt`:: a guarded command.  Blocks until `expr`