From 1fc8aa521934118b2e5aa7d07a939beaa58ee49a Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 24 Jun 2021 15:19:58 +0100 Subject: [PATCH 1/8] Implement getting arrays from the SMT2 backend This was previously unimplemented, which put null expressions into the trace steps and resulted in the elements of arrays not being printed when the trace is printed. --- src/solvers/smt2/smt2_conv.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 3b4fa14e4f0..1ac1735a837 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -319,6 +319,15 @@ exprt smt2_convt::get(const exprt &expr) const } else if(expr.is_constant()) return expr; + else if(const auto &array = expr_try_dynamic_cast(expr)) + { + exprt array_copy = *array; + for(auto &element : array_copy.operands()) + { + element = get(element); + } + return array_copy; + } return nil_exprt(); } From a865edef37ddd36cd8a7b335723eebec0b7c55b0 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Fri, 2 Jul 2021 17:01:59 +0100 Subject: [PATCH 2/8] Fixes array value in traces for Z3 SMT This is a fix for how we parse Z3 array output to reconstruct values in traces. This is specific bug fix for Z3 array output. --- src/solvers/smt2/smt2_conv.cpp | 83 ++++++++++++++++++++++++++++------ src/solvers/smt2/smt2_conv.h | 15 ++++++ 2 files changed, 84 insertions(+), 14 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 1ac1735a837..251155925b6 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -283,6 +283,7 @@ exprt smt2_convt::get(const exprt &expr) const if(it!=identifier_map.end()) return it->second.value; + return expr; } else if(expr.id()==ID_nondet_symbol) { @@ -473,31 +474,85 @@ constant_exprt smt2_convt::parse_literal( exprt smt2_convt::parse_array( const irept &src, const array_typet &type) +{ + std::unordered_map operands_map; + walk_array_tree(&operands_map, src, type); + exprt::operandst operands; + // Try to find the default value, if there is none then set it + auto maybe_default_op = operands_map.find(-1); + exprt default_op; + if(maybe_default_op == operands_map.end()) + default_op = nil_exprt(); + else + default_op = maybe_default_op->second; + int64_t i = 0; + auto maybe_size = numeric_cast(type.size()); + if(maybe_size.has_value()) + { + while(i < maybe_size.value()) + { + auto found_op = operands_map.find(i); + if(found_op != operands_map.end()) + operands.emplace_back(found_op->second); + else + operands.emplace_back(default_op); + i++; + } + } + else + { + // Array size is unknown, keep adding with known indexes in order + // until we fail to find one. + auto found_op = operands_map.find(i); + while(found_op != operands_map.end()) + { + operands.emplace_back(found_op->second); + i++; + found_op = operands_map.find(i); + } + operands.emplace_back(default_op); + } + return array_exprt(operands, type); +} + +void smt2_convt::walk_array_tree( + std::unordered_map *operands_map, + const irept &src, + const array_typet &type) { if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store") { + // This is the SMT syntax being parsed here // (store array index value) - if(src.get_sub().size()!=4) - return nil_exprt(); - - exprt array=parse_array(src.get_sub()[1], type); - exprt index=parse_rec(src.get_sub()[2], type.size().type()); - exprt value=parse_rec(src.get_sub()[3], type.subtype()); - - return with_exprt(array, index, value); + // Recurse + walk_array_tree(operands_map, src.get_sub()[1], type); + const auto index_expr = parse_rec(src.get_sub()[2], type.size().type()); + const constant_exprt index_constant = to_constant_expr(index_expr); + mp_integer tempint; + bool failure = to_integer(index_constant, tempint); + if(failure) + return; + long index = tempint.to_long(); + exprt value = parse_rec(src.get_sub()[3], type.subtype()); + operands_map->emplace(index, value); + } + else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let") + { + // This is produced by Z3 + // (let (....) (....)) + walk_array_tree( + operands_map, src.get_sub()[1].get_sub()[0].get_sub()[1], type); + walk_array_tree(operands_map, src.get_sub()[2], type); } else if(src.get_sub().size()==2 && src.get_sub()[0].get_sub().size()==3 && src.get_sub()[0].get_sub()[0].id()=="as" && src.get_sub()[0].get_sub()[1].id()=="const") { - // This is produced by Z3. - // ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x00))) - exprt value=parse_rec(src.get_sub()[1], type.subtype()); - return array_of_exprt(value, type); + // (as const type_info default_value) + exprt default_value = parse_rec(src.get_sub()[1], type.subtype()); + operands_map->emplace(-1, default_value); } - else - return nil_exprt(); } exprt smt2_convt::parse_union( diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index e1a65ff2fb5..0f5cb30c768 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -159,8 +159,23 @@ class smt2_convt : public stack_decision_proceduret constant_exprt parse_literal(const irept &, const typet &type); struct_exprt parse_struct(const irept &s, const struct_typet &type); exprt parse_union(const irept &s, const union_typet &type); + /// This function is for parsing array output from SMT solvers + /// when "(get-value |???|)" returns an array object. + /// \param s: is the irept parsed from the SMT output + /// \param type: is the expected type + /// \returns an exprt that represents the array exprt parse_array(const irept &s, const array_typet &type); exprt parse_rec(const irept &s, const typet &type); + /// This function walks the SMT output and populates a + /// map with index/value pairs for the array + /// \param operands_map: is a map of the operands to the array + /// being constructed indexed by their index. + /// \param src: is the irept source for the SMT output + /// \param type: is the type of the array + void walk_array_tree( + std::unordered_map *operands_map, + const irept &src, + const array_typet &type); // we use this to build a bit-vector encoding of the FPA theory void convert_floatbv(const exprt &expr); From 94fa314f0e475a5827e9418881b6aa7a4d05f32e Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Mon, 5 Jul 2021 10:34:16 +0100 Subject: [PATCH 3/8] Fix tests previously broken This removes the labels on some tests that used to have the broken-smt-backend flag but now pass. --- regression/cbmc/enum-trace1/test_json.desc | 2 +- regression/cbmc/json-interface1/test.desc | 2 +- regression/cbmc/json1/test.desc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/enum-trace1/test_json.desc b/regression/cbmc/enum-trace1/test_json.desc index 255c95b8c1c..6619fc73eea 100644 --- a/regression/cbmc/enum-trace1/test_json.desc +++ b/regression/cbmc/enum-trace1/test_json.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --json-ui --function test --trace activate-multi-line-match diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc index 5ea8fe3d74c..a15a7b20943 100644 --- a/regression/cbmc/json-interface1/test.desc +++ b/regression/cbmc/json-interface1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE --json-interface < test.json activate-multi-line-match diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc index bf66d83d928..b9eb6a30118 100644 --- a/regression/cbmc/json1/test.desc +++ b/regression/cbmc/json1/test.desc @@ -1,4 +1,4 @@ -CORE broken-smt-backend +CORE main.c --json-ui --stop-on-fail activate-multi-line-match From 50354d640c90b72155f3273346a53840b3a02086 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Tue, 6 Jul 2021 15:26:36 +0100 Subject: [PATCH 4/8] Add regression tests for array output with z3 Add two regression tests to check for array output in traces. --- regression/cbmc/z3/trace-char.c | 5 +++++ regression/cbmc/z3/trace-char.desc | 13 +++++++++++++ regression/cbmc/z3/trace.c | 5 +++++ regression/cbmc/z3/trace.desc | 13 +++++++++++++ 4 files changed, 36 insertions(+) create mode 100644 regression/cbmc/z3/trace-char.c create mode 100644 regression/cbmc/z3/trace-char.desc create mode 100644 regression/cbmc/z3/trace.c create mode 100644 regression/cbmc/z3/trace.desc diff --git a/regression/cbmc/z3/trace-char.c b/regression/cbmc/z3/trace-char.c new file mode 100644 index 00000000000..18308105a75 --- /dev/null +++ b/regression/cbmc/z3/trace-char.c @@ -0,0 +1,5 @@ +void main(int argc, char **argv) +{ + char arr[] = {'0', '1', '2', '3', '4', '5', '6', '7'}; + assert(arr[0] == '2'); +} diff --git a/regression/cbmc/z3/trace-char.desc b/regression/cbmc/z3/trace-char.desc new file mode 100644 index 00000000000..ee19e04f73b --- /dev/null +++ b/regression/cbmc/z3/trace-char.desc @@ -0,0 +1,13 @@ +CORE smt-backend broken-cprover-smt-backend +trace-char.c +--trace --smt2 --z3 +^EXIT=10$ +^SIGNAL=0$ +arr=\{ arr +arr=\{ '0', '1', '2', '3', '4', '5', '6', '7' \} +-- +arr=(assignment removed) +error running SMT2 solver +-- +Run cbmc with the --z3 and --trace options with arrays to confirm that +char arrays are displayed in traces. diff --git a/regression/cbmc/z3/trace.c b/regression/cbmc/z3/trace.c new file mode 100644 index 00000000000..7e842774d2c --- /dev/null +++ b/regression/cbmc/z3/trace.c @@ -0,0 +1,5 @@ +void main(int argc, char **argv) +{ + int arr[] = {0, 1, 2, 3, 4, 5, 6, 17}; + assert(arr[0] == 2); +} diff --git a/regression/cbmc/z3/trace.desc b/regression/cbmc/z3/trace.desc new file mode 100644 index 00000000000..3900217e56b --- /dev/null +++ b/regression/cbmc/z3/trace.desc @@ -0,0 +1,13 @@ +CORE smt-backend broken-cprover-smt-backend +trace.c +--trace --smt2 --z3 +^EXIT=10$ +^SIGNAL=0$ +arr=\{ arr +arr=\{ 0, 1, 2, 3, 4, 5, 6, 17 \} +-- +arr=(assignment removed) +error running SMT2 solver +-- +Run cbmc with the --z3 and --trace options with arrays to confirm that +int arrays are displayed in traces. From 6a861a14a03eaab97a7ff5aec35a6cdedfe5a0f3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 29 Jun 2021 15:04:53 +0100 Subject: [PATCH 5/8] Ignore quantifier errors running `get-value` commands with `z3` Due to how we call z3 it is possible to have values that contain quantifiers appear in the results. However, z3 cannot give a real value in response to a "(get-value |XXX|)" request. This catches these any simply ignores them, allowing the rest of the code to continue. Note that this becomes necessary to handle since cbmc now produces quantifiers in expressions sent to z3. --- src/solvers/smt2/smt2_dec.cpp | 31 +++++++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 5a2979707fb..fdff05823d9 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -175,17 +175,36 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) { // We ignore errors after UNSAT because get-value after check-sat // returns unsat will give an error. - if(res!=resultt::D_UNSATISFIABLE) + if(res != resultt::D_UNSATISFIABLE) { - messaget log{message_handler}; - log.error() << "SMT2 solver returned error message:\n" - << "\t\"" << parsed.get_sub()[1].id() << "\"" - << messaget::eom; - return decision_proceduret::resultt::D_ERROR; + const auto &message = id2string(parsed.get_sub()[1].id()); + // Special case error handling + if( + solver == solvert::Z3 && + message.find("must not contain quantifiers") != std::string::npos) + { + // We tried to "(get-value |XXXX|)" where |XXXX| is determined to + // include a quantified expression + // Nothing to do, this should be caught and value assigned by the + // set_to defaults later. + } + // Unhandled error, log the error and report it back up to caller + else + { + messaget log{message_handler}; + log.error() << "SMT2 solver returned error message:\n" + << "\t\"" << message << "\"" << messaget::eom; + return decision_proceduret::resultt::D_ERROR; + } } } } + // If the result is not satisfiable don't bother updating the assignments and + // values (since we didn't get any), just return. + if(res != resultt::D_SATISFIABLE) + return res; + for(auto &assignment : identifier_map) { std::string conv_id=convert_identifier(assignment.first); From 393d47ae9cca17d74164b72866aa98b86be33d08 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 30 Jun 2021 11:28:06 +0100 Subject: [PATCH 6/8] Use `set_to` to infer missing boolean identifier values This fixes some of the cases where `z3` returns an error instead of a value for some of the values cbmc is attempting to get. --- src/solvers/smt2/smt2_conv.cpp | 1 + src/solvers/smt2/smt2_conv.h | 4 ++++ src/solvers/smt2/smt2_dec.cpp | 27 ++++++++++++++++++++------- 3 files changed, 25 insertions(+), 7 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 251155925b6..21322120357 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -4415,6 +4415,7 @@ void smt2_convt::set_to(const exprt &expr, bool value) // This is a converted expression, we can just assert the literal name // since the expression is already defined out << found_literal->second; + set_values[found_literal->second] = value; } else { diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 0f5cb30c768..d233575d96d 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -250,6 +250,10 @@ class smt2_convt : public stack_decision_proceduret typedef std::map defined_expressionst; defined_expressionst defined_expressions; + /// The values which boolean identifiers have been `smt2_convt::set_to` or + /// in other words those which are asserted as true / false in the output + /// smt2 formula. + std::unordered_map set_values; defined_expressionst object_sizes; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index fdff05823d9..7f66b5cd870 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -139,7 +139,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) boolean_assignment.resize(no_boolean_variables, false); typedef std::unordered_map valuest; - valuest values; + valuest parsed_values; while(in) { @@ -167,7 +167,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) // ( (|some_integer| 0) ) // ( (|some_integer| (- 10)) ) - values[s0.id()]=s1; + parsed_values[s0.id()] = s1; } else if( parsed.id().empty() && parsed.get_sub().size() == 2 && @@ -207,16 +207,29 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) for(auto &assignment : identifier_map) { - std::string conv_id=convert_identifier(assignment.first); - const irept &value=values[conv_id]; - assignment.second.value=parse_rec(value, assignment.second.type); + std::string conv_id = convert_identifier(assignment.first); + const irept &value = parsed_values[conv_id]; + assignment.second.value = parse_rec(value, assignment.second.type); } // Booleans for(unsigned v=0; vsecond.id() == ID_true; + // Work out the value based on what set_to was called with. + const auto found_set_value = + set_values.find('|' + boolean_identifier + '|'); + if(found_set_value != set_values.end()) + return found_set_value->second; + // Old code used the computation + // const irept &value=values["B"+std::to_string(v)]; + // boolean_assignment[v]=(value.id()==ID_true); + return parsed_values[boolean_identifier].id() == ID_true; + }(); } return res; From 1b9bdb5d5959241b37e0f5ba0b4f38798be78a92 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Wed, 7 Jul 2021 14:25:10 +0100 Subject: [PATCH 7/8] Add regression test for new error handling Add a new regression test for error handling for z3 output that came from a Issue #5970 --- regression/cbmc/z3/Issue5970.c | 11 +++++++++++ regression/cbmc/z3/Issue5970.desc | 12 ++++++++++++ 2 files changed, 23 insertions(+) create mode 100644 regression/cbmc/z3/Issue5970.c create mode 100644 regression/cbmc/z3/Issue5970.desc diff --git a/regression/cbmc/z3/Issue5970.c b/regression/cbmc/z3/Issue5970.c new file mode 100644 index 00000000000..9831e79672e --- /dev/null +++ b/regression/cbmc/z3/Issue5970.c @@ -0,0 +1,11 @@ +#include + +void main() +{ + unsigned A, x[64]; + // clang-format off + __CPROVER_assume(0 <= A && A < 64); + __CPROVER_assume(__CPROVER_forall { int i ; (0 <= i && i < A) ==> x[i] >= 1 }); + // clang-format on + assert(x[0] > 0); +} diff --git a/regression/cbmc/z3/Issue5970.desc b/regression/cbmc/z3/Issue5970.desc new file mode 100644 index 00000000000..5c85d8d81d7 --- /dev/null +++ b/regression/cbmc/z3/Issue5970.desc @@ -0,0 +1,12 @@ +CORE smt-backend broken-cprover-smt-backend +Issue5970.c +--z3 +^EXIT=10$ +^SIGNAL=0$ +^\[main\.assertion\.1\] line [0-9]+ assertion x\[0\] > 0: FAILURE$ +-- +invalid get-value term, term must be ground and must not contain quantifiers +^\[main\.assertion\.1\] line [0-9]+ assertion x\[0\] > 0: ERROR$ +-- +This tests that attempts to "(get-value |XXX|)" from z3 sat results +are handled and do not cause an error message or ERROR result. From e66aa298886db7574d57b4a68e16297058fdce69 Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Wed, 7 Jul 2021 14:15:02 +0100 Subject: [PATCH 8/8] Fix tags on broken SMT backend test These various tests are either broken with error or timeout on SMT backends, in particular cprover-smt or z3. # Please enter the commit message for your changes. Lines starting --- regression/cbmc/Float-div3/test.desc | 2 +- regression/cbmc/Quantifiers-assertion/test.desc | 2 +- regression/cbmc/Quantifiers-assignment/test.desc | 2 +- regression/cbmc/Quantifiers-if/test.desc | 2 +- regression/cbmc/Quantifiers-initialisation2/test.desc | 2 +- regression/cbmc/Quantifiers-not-exists/fixed.desc | 2 +- regression/cbmc/Quantifiers-not/test.desc | 2 +- regression/cbmc/Quantifiers-two-dimension-array/test.desc | 2 +- regression/cbmc/union10/union_list2.desc | 2 +- regression/cbmc/union11/union_list.desc | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/regression/cbmc/Float-div3/test.desc b/regression/cbmc/Float-div3/test.desc index b7d95a28215..e40801d9f85 100644 --- a/regression/cbmc/Float-div3/test.desc +++ b/regression/cbmc/Float-div3/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c --floatbv ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 46ce7f990fa..b1a5226b9b1 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index a584f718857..91fdb54f4e1 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index 0797ac525b4..0269bf6e9a7 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index ab42e172aea..e841114af5f 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.desc b/regression/cbmc/Quantifiers-not-exists/fixed.desc index 6d41315fd94..4e784a1b684 100644 --- a/regression/cbmc/Quantifiers-not-exists/fixed.desc +++ b/regression/cbmc/Quantifiers-not-exists/fixed.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend fixed.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index 815e388b2d0..50b7285586e 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index f12ffbd5519..802c82dac74 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend main.c ^\*\* Results:$ diff --git a/regression/cbmc/union10/union_list2.desc b/regression/cbmc/union10/union_list2.desc index 613581a5fc8..88bd7d7090e 100644 --- a/regression/cbmc/union10/union_list2.desc +++ b/regression/cbmc/union10/union_list2.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend union_list2.c ^EXIT=0$ diff --git a/regression/cbmc/union11/union_list.desc b/regression/cbmc/union11/union_list.desc index e4d3a427794..4d4566283f4 100644 --- a/regression/cbmc/union11/union_list.desc +++ b/regression/cbmc/union11/union_list.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-z3-smt-backend union_list.c ^EXIT=0$