diff --git a/librumur/include/rumur/TypeExpr.h b/librumur/include/rumur/TypeExpr.h index 9d4189eb..a8592490 100644 --- a/librumur/include/rumur/TypeExpr.h +++ b/librumur/include/rumur/TypeExpr.h @@ -36,11 +36,10 @@ struct RUMUR_API_WITH_RTTI TypeExpr : public Node { virtual mpz_class count() const = 0; virtual Ptr resolve() const; - /* Numeric bounds of this type as valid C code. These are only valid to use on - * TypeExprs for which is_simple() returns true. - */ - virtual std::string lower_bound() const; - virtual std::string upper_bound() const; + // Numeric bounds of this type. These are only valid to use on TypeExprs for + // which is_simple() returns true. + virtual mpz_class lower_bound() const; + virtual mpz_class upper_bound() const; // Get a string representation of this type std::string to_string() const; @@ -81,8 +80,8 @@ struct RUMUR_API_WITH_RTTI Range : public TypeExpr { bool is_simple() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; }; @@ -101,8 +100,8 @@ struct RUMUR_API_WITH_RTTI Scalarset : public TypeExpr { bool is_simple() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; }; @@ -127,8 +126,8 @@ struct RUMUR_API_WITH_RTTI Enum : public TypeExpr { bool is_simple() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; bool is_boolean() const override; @@ -185,8 +184,8 @@ struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr { Ptr resolve() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; }; diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc index af062479..32f65580 100644 --- a/librumur/src/Expr.cc +++ b/librumur/src/Expr.cc @@ -1570,7 +1570,7 @@ std::string Quantifier::lower_bound() const { loc); if (type != nullptr) - return type->lower_bound(); + return "VALUE_C(" + type->lower_bound().get_str() + ")"; assert(from != nullptr && "quantifier with null type and null lower bound"); diff --git a/librumur/src/TypeExpr.cc b/librumur/src/TypeExpr.cc index 278ef3a5..680531f2 100644 --- a/librumur/src/TypeExpr.cc +++ b/librumur/src/TypeExpr.cc @@ -26,11 +26,11 @@ bool TypeExpr::is_simple() const { return false; } Ptr TypeExpr::resolve() const { return Ptr(clone()); } -std::string TypeExpr::lower_bound() const { +mpz_class TypeExpr::lower_bound() const { throw Error("complex types do not have valid lower bounds", loc); } -std::string TypeExpr::upper_bound() const { +mpz_class TypeExpr::upper_bound() const { throw Error("complex types do not have valid upper bounds", loc); } @@ -218,13 +218,9 @@ void Range::validate() const { throw Error("upper bound of range is less than lower bound", loc); } -std::string Range::lower_bound() const { - return "VALUE_C(" + min->constant_fold().get_str() + ")"; -} +mpz_class Range::lower_bound() const { return min->constant_fold(); } -std::string Range::upper_bound() const { - return "VALUE_C(" + max->constant_fold().get_str() + ")"; -} +mpz_class Range::upper_bound() const { return max->constant_fold(); } void Range::to_stream(std::ostream &out) const { out << *min << ".." << *max; } @@ -260,12 +256,9 @@ void Scalarset::validate() const { throw Error("bound of scalarset is not positive", bound->loc); } -std::string Scalarset::lower_bound() const { return "VALUE_C(0)"; } +mpz_class Scalarset::lower_bound() const { return 0; } -std::string Scalarset::upper_bound() const { - mpz_class b = bound->constant_fold() - 1; - return "VALUE_C(" + b.get_str() + ")"; -} +mpz_class Scalarset::upper_bound() const { return bound->constant_fold() - 1; } void Scalarset::to_stream(std::ostream &out) const { out << "scalarset(" << *bound << ")"; @@ -302,13 +295,13 @@ void Enum::validate() const { } } -std::string Enum::lower_bound() const { return "VALUE_C(0)"; } +mpz_class Enum::lower_bound() const { return 0; } -std::string Enum::upper_bound() const { +mpz_class Enum::upper_bound() const { mpz_class size = members.size(); if (size > 0) size--; - return "VALUE_C(" + size.get_str() + ")"; + return size; } void Enum::to_stream(std::ostream &out) const { @@ -464,13 +457,13 @@ void TypeExprID::validate() const { throw Error("unresolved type symbol \"" + name + "\"", loc); } -std::string TypeExprID::lower_bound() const { +mpz_class TypeExprID::lower_bound() const { if (referent == nullptr) throw Error("unresolved type symbol \"" + name + "\"", loc); return referent->value->lower_bound(); } -std::string TypeExprID::upper_bound() const { +mpz_class TypeExprID::upper_bound() const { if (referent == nullptr) throw Error("unresolved type symbol \"" + name + "\"", loc); return referent->value->upper_bound(); diff --git a/murphi2c/resources/c_prefix.c b/murphi2c/resources/c_prefix.c index 59f7f511..c3b1ae9e 100644 --- a/murphi2c/resources/c_prefix.c +++ b/murphi2c/resources/c_prefix.c @@ -41,32 +41,4 @@ static void liveness_(const char *message __attribute__((unused))) {} void (*liveness)(const char *) = liveness_; -// various printf wrappers to deal with the user having passed --value-type -static __attribute__((unused)) void print_int (int v) { printf("%d", v); } -static __attribute__((unused)) void print_unsigned(unsigned v) { printf("%u", v); } -static __attribute__((unused)) void print_short (short v) { printf("%hd", v); } -static __attribute__((unused)) void print_long (long v) { printf("%ld", v); } -static __attribute__((unused)) void print_int8_t (int8_t v) { printf("%" PRId8 , v); } -static __attribute__((unused)) void print_uint8_t (uint8_t v) { printf("%" PRIu8 , v); } -static __attribute__((unused)) void print_int16_t (int16_t v) { printf("%" PRId16, v); } -static __attribute__((unused)) void print_uint16_t(uint16_t v) { printf("%" PRIu16, v); } -static __attribute__((unused)) void print_int32_t (int32_t v) { printf("%" PRId32, v); } -static __attribute__((unused)) void print_uint32_t(uint32_t v) { printf("%" PRIu32, v); } -static __attribute__((unused)) void print_int64_t (int64_t v) { printf("%" PRId64, v); } -static __attribute__((unused)) void print_uint64_t(uint64_t v) { printf("%" PRIu64, v); } - -// wrappers for producing literal expressions of value type -#define int_VALUE_C(v) (v) -#define unsigned_VALUE_C(v) (v ## u) -#define short_VALUE_C(v) ((short)(v)) -#define long_VALUE_C(v) (v ## l) -#define int8_t_VALUE_C(v) INT8_C(v) -#define uint8_t_VALUE_C(v) UINT8_C(v) -#define int16_t_VALUE_C(v) INT16_C(v) -#define uint16_t_VALUE_C(v) UINT16_C(v) -#define int32_t_VALUE_C(v) INT32_C(v) -#define uint32_t_VALUE_C(v) UINT32_C(v) -#define int64_t_VALUE_C(v) INT64_C(v) -#define uint64_t_VALUE_C(v) UINT64_C(v) - diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index c070663c..96cb0908 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -13,6 +13,94 @@ using namespace rumur; +/// emit a typed C numeric literal +/// +/// Numeric literals are of type `int` in C by default. To spell a literal of a +/// different type, we need a bit of specialisation. This function is best +/// effort, in the sense that pathological input may result in an expression of +/// incorrect type. +/// +/// @param c_type The desired type of the resulting literal +/// @param v The value of the literal +/// @return C code that describes the given typed literal. +static std::string c_lit(const std::string &c_type, const mpz_class &v) { + const std::string s = v.get_str(); + if (c_type == "int") + return s; + if (c_type == "unsigned" || c_type == "unsigned int") + return s + "u"; + if (c_type == "long" || c_type == "long int" || c_type == "signed long" || + c_type == "signed long int") + return s + "l"; + if (c_type == "unsigned long" || c_type == "unsigned long int") + return s + "lu"; + if (c_type == "long long" || c_type == "long long int" || + c_type == "signed long long" || c_type == "signed long long int") + return s + "ll"; + if (c_type == "unsigned long long" || c_type == "unsigned long long int") + return s + "ull"; + if (c_type == "int8_t") + return "INT8_C(" + s + ")"; + if (c_type == "uint8_t") + return "UINT8_C(" + s + ")"; + if (c_type == "int16_t") + return "INT16_C(" + s + ")"; + if (c_type == "uint16_t") + return "UINT16_C(" + s + ")"; + if (c_type == "int32_t") + return "INT32_C(" + s + ")"; + if (c_type == "uint32_t") + return "UINT32_C(" + s + ")"; + if (c_type == "int64_t") + return "INT64_C(" + s + ")"; + if (c_type == "uint64_t") + return "UINT64_C(" + s + ")"; + + // otherwise assume we can construct the value with a cast + return "((" + c_type + ")" + s + ")"; +} + +/// get the printf format code for printing a given type +/// +/// See call sites of this function for why the return value includes stray +/// quote characters. +/// +/// @param c_type Type to print +/// @return Printf format code for this type +static const char *c_pri(const std::string &c_type) { + if (c_type == "unsigned" || c_type == "unsigned int") + return "u\""; + if (c_type == "long" || c_type == "long int" || c_type == "signed long" || + c_type == "signed long int") + return "ld\""; + if (c_type == "unsigned long" || c_type == "unsigned long int") + return "lu\""; + if (c_type == "long long" || c_type == "long long int" || + c_type == "signed long long" || c_type == "signed long long int") + return "lld\""; + if (c_type == "unsigned long long" || c_type == "unsigned long long int") + return "llu\""; + if (c_type == "int8_t") + return "\" PRId8"; + if (c_type == "uint8_t") + return "\" PRIu8"; + if (c_type == "int16_t") + return "\" PRId16"; + if (c_type == "uint16_t") + return "\" PRIu16"; + if (c_type == "int32_t") + return "\" PRId32"; + if (c_type == "uint32_t") + return "\" PRIu32"; + if (c_type == "int64_t") + return "\" PRId64"; + if (c_type == "uint64_t") + return "\" PRIu64"; + + // otherwise assume we can print this as an int + return "d\""; +} + void CLikeGenerator::visit_add(const Add &n) { *this << "(" << *n.lhs << " + " << *n.rhs << ")"; } @@ -115,9 +203,8 @@ void CLikeGenerator::visit_element(const Element &n) { auto a = dynamic_cast(t.get()); assert(a != nullptr && "non-array on LHS of array indexing expression"); - // find the lower bound of its index type, using some hacky mangling to align - // with one of the macros from ../resources/c_prefix.c - const std::string lb = value_type + "_" + a->index_type->lower_bound(); + // find the lower bound of its index type + const std::string lb = c_lit(value_type, a->index_type->lower_bound()); // emit an indexing operation, now account for this *this << "(" << *n.array << ".data[(" << *n.index << ") - " << lb << "])"; @@ -360,7 +447,7 @@ void CLikeGenerator::visit_neq(const Neq &n) { void CLikeGenerator::visit_not(const Not &n) { *this << "(!" << *n.rhs << ")"; } void CLikeGenerator::visit_number(const Number &n) { - *this << "((" << value_type << ")(" << n.value.get_str() << "))"; + *this << c_lit(value_type, n.value); } void CLikeGenerator::visit_or(const Or &n) { @@ -486,10 +573,9 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, // invent a unique symbol using our counter const std::string i = "array_index" + std::to_string(counter); - // get the bounds of the index and hackily prepend the value type to produce - // something corresponding to one of the macros in ../resources/c_prefix.c - const std::string lb = value_type + "_" + a->index_type->lower_bound(); - const std::string ub = value_type + "_" + a->index_type->upper_bound(); + // get the bounds of the index + const std::string lb = c_lit(value_type, a->index_type->lower_bound()); + const std::string ub = c_lit(value_type, a->index_type->upper_bound()); *this << indentation() << "for (size_t " << i << " = 0; ; ++" << i << ") {\n"; @@ -546,7 +632,8 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, } // fall back case, for Ranges and Scalarsets - *this << indentation() << "print_" << value_type << "(" << e << suffix << ")"; + *this << indentation() << "printf(\"%" << c_pri(value_type) << ", (" << e + << suffix << "))"; } void CLikeGenerator::visit_put(const Put &n) { diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc index f153cf6d..e0547498 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -108,10 +108,11 @@ class Generator : public ConstExprTraversal { } if (!lvalue && a.element_type->is_simple()) { - const std::string lb = a.element_type->lower_bound(); - const std::string ub = a.element_type->upper_bound(); + const std::string lb = a.element_type->lower_bound().get_str(); + const std::string ub = a.element_type->upper_bound().get_str(); *out << "handle_read(" << to_C_string(n.loc) << ", rule_name, " - << to_C_string(n) << ", s, " << lb << ", " << ub << ", "; + << to_C_string(n) << ", s, VALUE_C(" << lb << "), VALUE_C(" << ub + << "), "; } *out << "handle_index(" << to_C_string(n.loc) << ", rule_name, " @@ -177,8 +178,8 @@ class Generator : public ConstExprTraversal { assert((!n.is_lvalue() || t != nullptr) && "lvalue without a type"); if (!lvalue && n.is_lvalue() && t->is_simple()) { - const std::string lb = t->lower_bound(); - const std::string ub = t->upper_bound(); + const std::string lb = "VALUE_C(" + t->lower_bound().get_str() + ")"; + const std::string ub = "VALUE_C(" + t->upper_bound().get_str() + ")"; *out << "handle_read(" << to_C_string(n.loc) << ", rule_name, " << to_C_string(n) << ", s, " << lb << ", " << ub << ", "; } @@ -207,10 +208,11 @@ class Generator : public ConstExprTraversal { for (const Ptr &f : r->fields) { if (f->name == n.field) { if (!lvalue && f->type->is_simple()) { - const std::string lb = f->type->lower_bound(); - const std::string ub = f->type->upper_bound(); + const std::string lb = f->type->lower_bound().get_str(); + const std::string ub = f->type->upper_bound().get_str(); *out << "handle_read(" << to_C_string(n.loc) << ", rule_name, " - << to_C_string(n) << ", s, " << lb << ", " << ub << ", "; + << to_C_string(n) << ", s, VALUE_C(" << lb << "), VALUE_C(" + << ub << "), "; } *out << "handle_narrow("; if (lvalue) { @@ -304,6 +306,7 @@ class Generator : public ConstExprTraversal { * 5. We pass the original (rvalue) handle. */ + // clang-format off auto get_method = [](const Ptr ¶meter, const Ptr &argument) { @@ -325,6 +328,7 @@ class Generator : public ConstExprTraversal { assert(!"unreachable"); __builtin_unreachable(); }; + // clang-format on // Create the temporaries for each argument. { @@ -348,20 +352,20 @@ class Generator : public ConstExprTraversal { << ", .offset = 0, .width = " << p->width() << "ull }; "; if (method == 1) { - const std::string lb = p->get_type()->lower_bound(); - const std::string ub = p->get_type()->upper_bound(); + const std::string lb = p->get_type()->lower_bound().get_str(); + const std::string ub = p->get_type()->upper_bound().get_str(); *out << "handle_write(" << to_C_string(n.loc) << ", rule_name, " - << "\"\", s, " << lb << ", " << ub << ", " << handle - << ", "; + << "\"\", s, VALUE_C(" << lb << "), VALUE_C(" << ub + << "), " << handle << ", "; generate_rvalue(*out, *a); *out << "); "; } else if (method == 2) { - const std::string lb = p->get_type()->lower_bound(); - const std::string ub = p->get_type()->upper_bound(); + const std::string lb = p->get_type()->lower_bound().get_str(); + const std::string ub = p->get_type()->upper_bound().get_str(); - const std::string lba = a->type()->lower_bound(); + const std::string lba = a->type()->lower_bound().get_str(); *out << "{ " << "raw_value_t v = handle_read_raw(s, "; @@ -369,17 +373,18 @@ class Generator : public ConstExprTraversal { *out << "); " << "raw_value_t v2; " << "value_t v3; " - << "static const value_t lb = " << lb << "; " - << "static const value_t ub = " << ub << "; " - << "if (v != 0 && (SUB(v, 1, &v2) || ADD(v2, " << lba - << ", &v3) " + << "static const value_t lb = VALUE_C(" << lb << "); " + << "static const value_t ub = VALUE_C(" << ub << "); " + << "if (v != 0 && (SUB(v, 1, &v2) || ADD(v2, VALUE_C(" << lba + << "), &v3) " << "|| v3 < lb || v3 > ub)) { " << "error(s, \"call to function %s passed an out-of-range value " << "%\" PRIRAWVAL \" to parameter " << (index + 1) << "\", \"" - << n.name << "\", raw_value_to_string(v + " << lba << " - 1)); " + << n.name << "\", raw_value_to_string(v + VALUE_C(" << lba + << ") - 1)); " << "} " << "handle_write_raw(s, " << handle << ", v == 0 ? v : " - << "((raw_value_t)(v3 - " << lb << ") + 1)); " + << "((raw_value_t)(v3 - VALUE_C(" << lb << ")) + 1)); " << "} "; } else if (method == 3) { diff --git a/rumur/src/generate-print.cc b/rumur/src/generate-print.cc index 3084dde9..af3d31f9 100644 --- a/rumur/src/generate-print.cc +++ b/rumur/src/generate-print.cc @@ -360,8 +360,8 @@ class Generator : public ConstTypeTraversal { void visit_range(const Range &n) final { - const std::string lb = n.lower_bound(); - const std::string ub = n.upper_bound(); + const std::string lb = "VALUE_C(" + n.lower_bound().get_str() + ")"; + const std::string ub = "VALUE_C(" + n.upper_bound().get_str() + ")"; *out << "{\n" << " raw_value_t v = handle_read_raw(s, " << current_handle << ");\n" diff --git a/rumur/src/generate-quantifier.cc b/rumur/src/generate-quantifier.cc index a3125bd9..820d092f 100644 --- a/rumur/src/generate-quantifier.cc +++ b/rumur/src/generate-quantifier.cc @@ -37,7 +37,7 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { assert(q.from != nullptr); generate_rvalue(out, *q.from); } else { - out << q.type->lower_bound(); + out << "VALUE_C(" << q.type->lower_bound().get_str() << ")"; } out << ";\n"; @@ -46,7 +46,7 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { assert(q.to != nullptr); generate_rvalue(out, *q.to); } else { - out << q.type->upper_bound(); + out << "VALUE_C(" << q.type->upper_bound().get_str() << ")"; } out << ";\n"; @@ -88,19 +88,17 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { // bounds. References to this quantified variable will use these when // unpacking its compressed representation, so we need to offset the values we // store from it. - const std::string lower = q.decl->type->lower_bound(); - const std::string upper = q.decl->type->upper_bound(); + const std::string lower = q.decl->type->lower_bound().get_str(); + const std::string upper = q.decl->type->upper_bound().get_str(); out << "#if !defined(__clang__) && defined(__GNUC__)\n" << " #pragma GCC diagnostic push\n" << " #pragma GCC diagnostic ignored \"-Wtype-limits\"\n" << "#endif\n" - << " ASSERT(lb >= " << lower << " && lb <= " << upper - << " && " - "\"iteration lower bound exceeds type limits\");\n" - << " ASSERT(ub >= " << lower << " && ub <= " << upper - << " && " - "\"iteration upper bound exceeds type limits\");\n" + << " ASSERT(lb >= VALUE_C(" << lower << ") && lb <= VALUE_C(" << upper + << ") && \"iteration lower bound exceeds type limits\");\n" + << " ASSERT(ub >= VALUE_C(" << lower << ") && ub <= VALUE_C(" << upper + << ") && \"iteration upper bound exceeds type limits\");\n" << "#if !defined(__clang__) && defined(__GNUC__)\n" << " #pragma GCC diagnostic pop\n" << "#endif\n"; @@ -109,11 +107,12 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { // value we have is in range #define V_TO_RV(x) \ ("((raw_value_t)((raw_value_t)(((raw_value_t)" + std::string(x) + \ - ") + (raw_value_t)1) - (raw_value_t)(" + q.decl->type->lower_bound() + \ - ")))") + ") + (raw_value_t)1) - (raw_value_t)(VALUE_C(" + \ + q.decl->type->lower_bound().get_str() + "))))") #define RV_TO_V(x) \ - ("((value_t)(" + std::string(x) + " - (raw_value_t)1 + (raw_value_t)(" + \ - q.decl->type->lower_bound() + ")))") + ("((value_t)(" + std::string(x) + \ + " - (raw_value_t)1 + (raw_value_t)(VALUE_C(" + \ + q.decl->type->lower_bound().get_str() + "))))") // construct the pieces of our for-loop header const std::string init = "raw_value_t " + counter + " = " + V_TO_RV("lb"); diff --git a/rumur/src/generate-stmt.cc b/rumur/src/generate-stmt.cc index 70b60be0..12bb48ef 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -106,11 +106,12 @@ class Generator : public ConstStmtTraversal { void visit_assignment(const Assignment &s) final { if (s.lhs->type()->is_simple()) { - const std::string lb = s.lhs->type()->lower_bound(); - const std::string ub = s.lhs->type()->upper_bound(); + const std::string lb = s.lhs->type()->lower_bound().get_str(); + const std::string ub = s.lhs->type()->upper_bound().get_str(); *out << "handle_write(" << to_C_string(s.loc) << ", rule_name, " - << to_C_string(*s.lhs) << ", s, " << lb << ", " << ub << ", "; + << to_C_string(*s.lhs) << ", s, VALUE_C(" << lb << "), VALUE_C(" + << ub << "), "; generate_lvalue(*out, *s.lhs); *out << ", "; generate_rvalue(*out, *s.rhs); diff --git a/tests/tests.py b/tests/tests.py index cacc63f4..5da8a684 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1366,6 +1366,87 @@ def test_murphi2c_header(model, tmp_path): assert ret == 0, "C++ compilation failed:\n{}{}".format(stdout, stderr) +def test_murphi2c_type_with_space(): + """can murphi2c handle a `--value-type` with a space in it?""" + + # an arbitrary model using array indices + src = """\ + var x: array[0..1] of boolean; + + startstate begin + x[0] := true; + end; + + rule begin + x[0] := !x[0]; + end; + """ + + # run this through murphi2c with a `--value-type` with a space + args = ["murphi2c", "--value-type=signed char"] + if has_valgrind(): + args = [ + "valgrind", + "--leak-check=full", + "--show-leak-kinds=all", + "--error-exitcode=42", + "--", + ] + args + ret, stdout, stderr = run(args, src) + if has_valgrind(): + assert ret != 42, "Memory leak:\n{}{}".format(stdout, stderr) + + assert ret == 0, "Unexpected murphi2c exit:\n{}{}".format(stdout, stderr) + + # ask the C compiler if the source is valid + args = [cc()] + c_flags() + ["-c", "-o", os.devnull, "-"] + ret, out, err = run(args, stdout) + assert ret == 0, "C compilation failed:\n{}{}\nProgram:\n{}".format( + out, err, stdout + ) + + +def test_murphi2c_type_with_space2(): + """can murphi2c handle a `--value-type` with a space in it?""" + + # an arbitrary model using printing + src = """\ + var x: 0..1; + + startstate begin + x := 0; + end; + + rule begin + x := 1 - x; + put x; + end; + """ + + # run this through murphi2c with a `--value-type` with a space + args = ["murphi2c", "--value-type=signed char"] + if has_valgrind(): + args = [ + "valgrind", + "--leak-check=full", + "--show-leak-kinds=all", + "--error-exitcode=42", + "--", + ] + args + ret, stdout, stderr = run(args, src) + if has_valgrind(): + assert ret != 42, "Memory leak:\n{}{}".format(stdout, stderr) + + assert ret == 0, "Unexpected murphi2c exit:\n{}{}".format(stdout, stderr) + + # ask the C compiler if the source is valid + args = [cc()] + c_flags() + ["-c", "-o", os.devnull, "-"] + ret, out, err = run(args, stdout) + assert ret == 0, "C compilation failed:\n{}{}\nProgram:\n{}".format( + out, err, stdout + ) + + @pytest.mark.parametrize("model", MODELS) def test_murphi2xml(model): """test cases for murphi2xml"""