package info
(click to toggle)
Folder: tests
 |
.. (parent) | |||
|
d | rwxr-xr-x | 119 | disabled |
|
d | rwxr-xr-x | 70 | murphi-comment-ls |
 |
- | rw-r--r-- | 1,021 | 193.m |
|
- | rw-r--r-- | 656 | README.rst |
|
- | rw-r--r-- | 391 | alias-and-field.m |
|
- | rw-r--r-- | 365 | alias-in-bound.m |
|
- | rw-r--r-- | 283 | alias-in-bound2.m |
|
- | rw-r--r-- | 256 | alias-literal.m |
|
- | rw-r--r-- | 660 | alias-of-alias-rule.m |
|
- | rw-r--r-- | 224 | alias-of-alias-rule2.m |
|
- | rw-r--r-- | 179 | alias-of-alias-stmt.m |
|
- | rw-r--r-- | 131 | amp-amp-and.m |
|
- | rw-r--r-- | 182 | and-mixed.m |
|
- | rw-r--r-- | 719 | and-return.m |
|
- | rw-r--r-- | 4,133 | apartment.m |
|
- | rw-r--r-- | 243 | arithmetic-on-heterogeneous-ranges.m |
|
- | rw-r--r-- | 213 | array-assignment.m |
|
- | rw-r--r-- | 224 | assert-record.m |
|
- | rw-r--r-- | 217 | assert-syntax.m |
|
- | rw-r--r-- | 384 | assertion-type-limits.m |
|
- | rw-r--r-- | 218 | assume-in-ruleset.m |
|
- | rw-r--r-- | 139 | assume-statement.m |
|
- | rw-r--r-- | 403 | assume-statement2.m |
|
- | rw-r--r-- | 360 | assume-statement3.m |
|
- | rw-r--r-- | 422 | assume-statement4.m |
|
- | rw-r--r-- | 389 | bad-alias.m |
|
- | rw-r--r-- | 381 | bad-array-index.m |
|
- | rw-r--r-- | 253 | bad-element-lhs-in-or.m |
|
- | rw-r--r-- | 569 | bad-enum-print.m |
|
- | rw-r--r-- | 241 | bad-expr-type-ref.m |
|
- | rw-r--r-- | 719 | bad-field-lhs-in-or.m |
|
- | rw-r--r-- | 397 | bad-field.m |
|
- | rw-r--r-- | 428 | bad-function-call.m |
|
- | rw-r--r-- | 527 | bad-function-parameter.m |
|
- | rw-r--r-- | 705 | bad-invariant-number.m |
|
- | rw-r--r-- | 269 | bad-lvalue.m |
|
- | rw-r--r-- | 107 | basic-aliasrule.m |
|
- | rw-r--r-- | 122 | basic-const.m |
|
- | rw-r--r-- | 146 | basic-invariant.m |
|
- | rw-r--r-- | 137 | basic-ruleset.m |
|
- | rw-r--r-- | 114 | basic-ruleset2.m |
|
- | rw-r--r-- | 421 | basic-sandbox.m |
|
- | rw-r--r-- | 602 | bfs-vs-dfs.m |
|
- | rw-r--r-- | 176 | bitwise-and-enum.m |
|
- | rw-r--r-- | 195 | bitwise-and.m |
|
- | rw-r--r-- | 204 | bitwise-not-enum.m |
|
- | rw-r--r-- | 362 | bitwise-not.m |
|
- | rw-r--r-- | 176 | bitwise-or-enum.m |
|
- | rw-r--r-- | 225 | bitwise-or.m |
|
- | rw-r--r-- | 176 | bitwise-xor-enum.m |
|
- | rw-r--r-- | 260 | bitwise-xor.m |
|
- | rw-r--r-- | 297 | boolean-array-index.m |
|
- | rw-r--r-- | 213 | boolean-array.m |
|
- | rw-r--r-- | 162 | boolean-case.m |
|
- | rw-r--r-- | 877 | boolean-const.m |
|
- | rw-r--r-- | 463 | boolean-literal-case.m |
|
- | rw-r--r-- | 242 | boolean-shadow.m |
|
- | rw-r--r-- | 253 | bound-basic.m |
|
- | rw-r--r-- | 194 | bound-illegal.m |
|
- | rw-r--r-- | 269 | bound-limit.m |
|
- | rw-r--r-- | 308 | bound-limit2.m |
|
- | rw-r--r-- | 242 | bound-unused.m |
|
- | rw-r--r-- | 634 | call-no-lvalue.m |
|
- | rw-r--r-- | 324 | cex-boolean-startstate.m |
|
- | rw-r--r-- | 321 | cex-boolean.m |
|
- | rw-r--r-- | 345 | cex-enum-startstate.m |
|
- | rw-r--r-- | 549 | cex-enum.m |
|
- | rw-r--r-- | 180 | clear-complex.m |
|
- | rw-r--r-- | 161 | clear-simple.m |
|
- | rw-r--r-- | 530 | comment-escape.m |
|
- | rw-r--r-- | 390 | compare-array.m |
|
- | rw-r--r-- | 364 | compare-record.m |
|
- | rw-r--r-- | 370 | const-enum.m |
|
- | rw-r--r-- | 209 | const-folding.m |
|
- | rw-r--r-- | 201 | const-folding2.m |
|
- | rw-r--r-- | 201 | const-folding3.m |
|
- | rw-r--r-- | 201 | const-folding4.m |
|
- | rw-r--r-- | 202 | const-folding5.m |
|
- | rw-r--r-- | 202 | const-folding6.m |
|
- | rw-r--r-- | 243 | const-of-function-call.m |
|
- | rw-r--r-- | 142 | cover-basic.m |
|
- | rw-r--r-- | 321 | cover-basic2.m |
|
- | rw-r--r-- | 259 | cover-miss.m |
|
- | rw-r--r-- | 304 | cover-multiple.m |
|
- | rw-r--r-- | 271 | cover-stmt-miss.m |
|
- | rw-r--r-- | 254 | cover-stmt.m |
|
- | rw-r--r-- | 237 | cover-trivial.m |
|
- | rw-r--r-- | 899 | diff-trace-arrays.m |
|
- | rw-r--r-- | 130 | differing-range-passed-to-function.m |
|
- | rw-r--r-- | 456 | differing-type-return.m |
|
- | rw-r--r-- | 286 | differing-type-return3.m |
|
- | rw-r--r-- | 261 | division.m |
|
- | rw-r--r-- | 324 | double-semicolon.m |
|
- | rw-r--r-- | 161 | double-semicolon2.m |
|
- | rw-r--r-- | 327 | duplicate-enum-members.m |
|
- | rw-r--r-- | 252 | duplicate-enum-members2.m |
|
- | rw-r--r-- | 287 | duplicate-record-fields.m |
|
- | rw-r--r-- | 273 | duplicate-startstate.m |
|
- | rw-r--r-- | 204 | duplicate-state-fields.m |
|
- | rw-r--r-- | 261 | enum-local-var.m |
|
- | rw-r--r-- | 162 | error-statement.m |
|
- | rw-r--r-- | 501 | error-string-injection.m |
|
- | rw-r--r-- | 506 | escaping-expressions.m |
|
- | rw-r--r-- | 337 | for-step-0-dynamic.m |
|
- | rw-r--r-- | 234 | for-step-0.m |
|
- | rw-r--r-- | 231 | for-step-1.m |
|
- | rw-r--r-- | 251 | for-step-neg-1.m |
|
- | rw-r--r-- | 949 | for-step-neg-overflow.m |
|
- | rw-r--r-- | 484 | for-step-neg-overflow2.m |
|
- | rw-r--r-- | 186 | for-step-neg.m |
|
- | rw-r--r-- | 2,956 | for-variants.m |
|
- | rw-r--r-- | 2,573 | fox-goose-beans.m |
|
- | rw-r--r-- | 342 | function-and-field.m |
|
- | rw-r--r-- | 464 | function-call-in-if.m |
|
- | rw-r--r-- | 1,175 | function-in-guard.m |
|
- | rw-r--r-- | 876 | function-modifying.m |
|
- | rw-r--r-- | 227 | function-modifying2.m |
|
- | rw-r--r-- | 300 | function-order.m |
|
- | rw-r--r-- | 393 | function-param-intact.m |
|
- | rw-r--r-- | 291 | function-return-ignored.m |
|
- | rw-r--r-- | 283 | function1.m |
|
- | rw-r--r-- | 215 | identifier-case.m |
|
- | rw-r--r-- | 217 | identifier-case2.m |
|
- | rw-r--r-- | 272 | identifier-case3.m |
|
- | rw-r--r-- | 351 | illegal-array-index.m |
|
- | rw-r--r-- | 164 | index-out-of-range.m |
|
- | rw-r--r-- | 324 | invariant-failure-message.m |
|
- | rw-r--r-- | 189 | invariant-syntax.m |
|
- | rw-r--r-- | 197 | isundefined-array.m |
|
- | rw-r--r-- | 269 | isundefined-basic.m |
|
- | rw-r--r-- | 414 | isundefined-decl.m |
|
- | rw-r--r-- | 291 | isundefined-element.m |
|
- | rw-r--r-- | 740 | isundefined-function.m |
|
- | rw-r--r-- | 199 | isundefined-record.m |
|
- | rw-r--r-- | 177 | isundefined-rvalue.m |
|
- | rw-r--r-- | 175 | isundefined-rvalue2.m |
|
- | rw-r--r-- | 306 | keyword-case.m |
|
- | rw-r--r-- | 233 | liveness-in-ruleset.m |
|
- | rw-r--r-- | 348 | liveness-in-ruleset2.m |
|
- | rw-r--r-- | 317 | liveness-miss1.m |
|
- | rw-r--r-- | 336 | liveness-miss2.m |
|
- | rw-r--r-- | 357 | liveness-miss3.m |
|
- | rw-r--r-- | 253 | liveness-statement.m |
|
- | rw-r--r-- | 529 | loop-variable-nonzero-start.m |
|
- | rw-r--r-- | 879 | lsh-basic.m |
|
- | rw-r--r-- | 166 | lsh-boolean.m |
|
- | rw-r--r-- | 182 | lsh-boolean2.m |
|
- | rw-r--r-- | 170 | lsh-enum.m |
|
- | rw-r--r-- | 179 | lsh-enum2.m |
|
- | rw-r--r-- | 253 | math-operators.m |
|
- | rw-r--r-- | 1,139 | mixed-aliases.m |
|
- | rw-r--r-- | 199 | mod-neg-1.m |
|
- | rw-r--r-- | 193 | mod-neg-1_2.m |
|
- | rw-r--r-- | 153 | multiple-const-decl.m |
|
- | rw-r--r-- | 1,252 | multiple-deadlocks.m |
|
- | rw-r--r-- | 409 | multiple-errors.m |
|
- | rw-r--r-- | 161 | multiple-parameters.m |
|
- | rw-r--r-- | 239 | multiple-parameters2.m |
|
- | rw-r--r-- | 169 | multiple-type-decls.m |
|
- | rw-r--r-- | 281 | multiplication.m |
|
- | rw-r--r-- | 159 | named-assert.m |
|
- | rw-r--r-- | 542 | negate-complex.m |
|
- | rw-r--r-- | 645 | negate-value-type.m |
|
- | rw-r--r-- | 268 | negation-of-range.m |
|
- | rw-r--r-- | 185 | negative-numbers.m |
|
- | rw-r--r-- | 429 | no-cex-bug.m |
|
- | rw-r--r-- | 396 | no-cex-bug2.m |
|
- | rw-r--r-- | 204 | non-boolean-condition.m |
|
- | rw-r--r-- | 506 | non-const-parameters.m |
|
- | rw-r--r-- | 155 | octal-literal.m |
|
- | rw-r--r-- | 345 | octal-literal2.m |
|
- | rw-r--r-- | 82 | only-booleans.m |
|
- | rw-r--r-- | 157 | only-enum.m |
|
- | rw-r--r-- | 240 | only-range-and-array.m |
|
- | rw-r--r-- | 159 | only-range-and-untouched-array.m |
|
- | rw-r--r-- | 145 | only-range-and-unused-array.m |
|
- | rw-r--r-- | 182 | or-mixed.m |
|
- | rw-r--r-- | 181 | or-return.m |
|
- | rw-r--r-- | 355 | out-of-range-function-parameter.m |
|
- | rw-r--r-- | 428 | out-of-range-function-parameter2.m |
|
- | rw-r--r-- | 191 | pack-state-off.m |
|
- | rw-r--r-- | 131 | pipe-pipe-or.m |
|
- | rw-r--r-- | 428 | procedure-call-in-expr.m |
|
- | rw-r--r-- | 162 | put-stmt.m |
|
- | rw-r--r-- | 283 | put-stmt2.m |
|
- | rw-r--r-- | 147 | put-stmt3.m |
|
- | rw-r--r-- | 1,755 | put-stmt4.m |
|
- | rw-r--r-- | 509 | put-string-injection.m |
|
- | rw-r--r-- | 634 | quantifier-signed-range.m |
|
- | rw-r--r-- | 440 | range-and.m |
|
- | rw-r--r-- | 363 | read-slice.m |
|
- | rw-r--r-- | 134 | read-undefined.m |
|
- | rw-r--r-- | 166 | read-undefined2.m |
|
- | rw-r--r-- | 163 | read-undefined3.m |
|
- | rw-r--r-- | 379 | recursion1.m |
|
- | rw-r--r-- | 342 | recursion2.m |
|
- | rw-r--r-- | 399 | recursion3.m |
|
- | rw-r--r-- | 792 | recursion4.m |
|
- | rw-r--r-- | 365 | recursion5.m |
|
- | rw-r--r-- | 146 | reference-function-parameter.m |
|
- | rw-r--r-- | 150 | reference-function-parameter2.m |
|
- | rw-r--r-- | 155 | reference-function-parameter3.m |
|
- | rw-r--r-- | 455 | regression-bad-assumption-check.m |
|
- | rw-r--r-- | 236 | return-expression-from-rule.m |
|
- | rw-r--r-- | 217 | return-from-rule.m |
|
- | rw-r--r-- | 270 | return-from-ruleset.m |
|
- | rw-r--r-- | 223 | return-from-startstate.m |
|
- | rw-r--r-- | 462 | return-record-in-guard.m |
|
- | rw-r--r-- | 454 | rsh-and.m |
|
- | rw-r--r-- | 965 | rsh-basic.m |
|
- | rw-r--r-- | 167 | rsh-boolean.m |
|
- | rw-r--r-- | 183 | rsh-boolean2.m |
|
- | rw-r--r-- | 171 | rsh-enum.m |
|
- | rw-r--r-- | 180 | rsh-enum2.m |
|
- | rw-r--r-- | 278 | rule-duplicate-name.m |
|
- | rw-r--r-- | 267 | ruleset-invariant.m |
|
- | rw-r--r-- | 112 | ruleset-startstate.m |
|
- | rw-r--r-- | 752 | ruleset-trace.m |
|
- | rw-r--r-- | 844 | ruleset-trace2.m |
|
- | rw-r--r-- | 523 | ruleset-trace3.m |
|
- | rw-r--r-- | 552 | scalarset-cex.m |
|
- | rw-r--r-- | 780 | scalarset-put.m |
|
- | rw-r--r-- | 653 | scalarset-schedules-off-2.m |
|
- | rw-r--r-- | 763 | scalarset-schedules-off.m |
|
- | rw-r--r-- | 285 | scalarset-trivial.m |
|
- | rw-r--r-- | 631 | scalarset-undefined.m |
|
- | rw-r--r-- | 236 | section-order.m |
|
- | rw-r--r-- | 912 | section-order10.m |
|
- | rw-r--r-- | 210 | section-order2.m |
|
- | rw-r--r-- | 167 | section-order3.m |
|
- | rw-r--r-- | 200 | section-order4.m |
|
- | rw-r--r-- | 213 | section-order5.m |
|
- | rw-r--r-- | 228 | section-order6.m |
|
- | rw-r--r-- | 214 | section-order7.m |
|
- | rw-r--r-- | 244 | section-order8.m |
|
- | rw-r--r-- | 250 | section-order9.m |
|
- | rw-r--r-- | 116 | simple-deadlock.m |
|
- | rw-r--r-- | 414 | smart-quotes.m |
|
- | rw-r--r-- | 399 | smt-add.m |
|
- | rw-r--r-- | 541 | smt-array-bool-index.m |
|
- | rw-r--r-- | 550 | smt-array-bool-value-and-index.m |
|
- | rw-r--r-- | 534 | smt-array-bool-value.m |
|
- | rw-r--r-- | 538 | smt-array-enum-index.m |
|
- | rw-r--r-- | 516 | smt-array-enum-index2.m |
|
- | rw-r--r-- | 556 | smt-array-enum-value-and-index.m |
|
- | rw-r--r-- | 542 | smt-array-enum-value-and-index2.m |
|
- | rw-r--r-- | 537 | smt-array-enum-value.m |
|
- | rw-r--r-- | 511 | smt-array-enum-value2.m |
|
- | rw-r--r-- | 465 | smt-array-of-record.m |
|
- | rw-r--r-- | 506 | smt-array-range.m |
|
- | rw-r--r-- | 499 | smt-array-range2.m |
|
- | rw-r--r-- | 762 | smt-bool-literal.m |
|
- | rw-r--r-- | 434 | smt-bv-add.m |
|
- | rw-r--r-- | 442 | smt-bv-band.m |
|
- | rw-r--r-- | 391 | smt-bv-bitwise-not.m |
|
- | rw-r--r-- | 446 | smt-bv-bor.m |
|
- | rw-r--r-- | 434 | smt-bv-div.m |
|
- | rw-r--r-- | 446 | smt-bv-div2.m |
|
- | rw-r--r-- | 470 | smt-bv-exists.m |
|
- | rw-r--r-- | 485 | smt-bv-exists2.m |
|
- | rw-r--r-- | 473 | smt-bv-exists3.m |
|
- | rw-r--r-- | 479 | smt-bv-exists4.m |
|
- | rw-r--r-- | 478 | smt-bv-forall.m |
|
- | rw-r--r-- | 493 | smt-bv-forall2.m |
|
- | rw-r--r-- | 481 | smt-bv-forall3.m |
|
- | rw-r--r-- | 486 | smt-bv-forall4.m |
|
- | rw-r--r-- | 422 | smt-bv-geq.m |
|
- | rw-r--r-- | 419 | smt-bv-gt.m |
|
- | rw-r--r-- | 422 | smt-bv-leq.m |
|
- | rw-r--r-- | 445 | smt-bv-lsh.m |
|
- | rw-r--r-- | 420 | smt-bv-lt.m |
|
- | rw-r--r-- | 432 | smt-bv-mod.m |
|
- | rw-r--r-- | 441 | smt-bv-mod2.m |
|
- | rw-r--r-- | 442 | smt-bv-mul.m |
|
- | rw-r--r-- | 430 | smt-bv-neg.m |
|
- | rw-r--r-- | 312 | smt-bv-negative-literal.m |
|
- | rw-r--r-- | 446 | smt-bv-rsh.m |
|
- | rw-r--r-- | 437 | smt-bv-sub.m |
|
- | rw-r--r-- | 448 | smt-bv-xor.m |
|
- | rw-r--r-- | 529 | smt-const.m |
|
- | rw-r--r-- | 399 | smt-div.m |
|
- | rw-r--r-- | 430 | smt-enum-typeexprid.m |
|
- | rw-r--r-- | 434 | smt-enum.m |
|
- | rw-r--r-- | 442 | smt-enum2-typeexprid.m |
|
- | rw-r--r-- | 465 | smt-enum2-typeexprid2.m |
|
- | rw-r--r-- | 432 | smt-enum2.m |
|
- | rw-r--r-- | 465 | smt-exists.m |
|
- | rw-r--r-- | 473 | smt-exists2.m |
|
- | rw-r--r-- | 457 | smt-exists3.m |
|
- | rw-r--r-- | 477 | smt-exists4.m |
|
- | rw-r--r-- | 473 | smt-forall.m |
|
- | rw-r--r-- | 481 | smt-forall2.m |
|
- | rw-r--r-- | 465 | smt-forall3.m |
|
- | rw-r--r-- | 484 | smt-forall4.m |
|
- | rw-r--r-- | 387 | smt-geq.m |
|
- | rw-r--r-- | 384 | smt-gt.m |
|
- | rw-r--r-- | 387 | smt-leq.m |
|
- | rw-r--r-- | 385 | smt-lt.m |
|
- | rw-r--r-- | 397 | smt-mod.m |
|
- | rw-r--r-- | 407 | smt-mul.m |
|
- | rw-r--r-- | 395 | smt-neg.m |
|
- | rw-r--r-- | 700 | smt-negative-literal.m |
|
- | rw-r--r-- | 536 | smt-nested-array.m |
|
- | rw-r--r-- | 436 | smt-range.m |
|
- | rw-r--r-- | 533 | smt-record-bool-field.m |
|
- | rw-r--r-- | 489 | smt-record-bool-field2.m |
|
- | rw-r--r-- | 537 | smt-record-enum-field.m |
|
- | rw-r--r-- | 519 | smt-record-enum-field2.m |
|
- | rw-r--r-- | 465 | smt-record-of-array.m |
|
- | rw-r--r-- | 531 | smt-record-range-field.m |
|
- | rw-r--r-- | 513 | smt-record-range-field2.m |
|
- | rw-r--r-- | 715 | smt-shadowed-decl.m |
|
- | rw-r--r-- | 506 | smt-simplify.m |
|
- | rw-r--r-- | 402 | smt-sub.m |
|
- | rw-r--r-- | 740 | smt-typedecl-boolean.m |
|
- | rw-r--r-- | 287 | smt-typeexprid.m |
|
- | rw-r--r-- | 297 | smt-typeexprid2.m |
|
- | rw-r--r-- | 1,037 | state-reorder.m |
|
- | rw-r--r-- | 177 | string-escape1.m |
|
- | rw-r--r-- | 155 | string-escape2.m |
|
- | rw-r--r-- | 157 | string-escape3.m |
|
- | rw-r--r-- | 418 | string-injection.m |
|
- | rw-r--r-- | 318 | switch-nested.m |
|
- | rw-r--r-- | 1,269 | switch-stmt1.m |
|
- | rw-r--r-- | 305 | switch-stmt2.m |
|
- | rw-r--r-- | 378 | switch-stmt3.m |
|
- | rw-r--r-- | 228 | ternary-operator.m |
|
- | rw-r--r-- | 69,852 | tests.py |
|
- | rw-r--r-- | 218 | trivial-function.m |
|
- | rw-r--r-- | 454 | two-enums.m |
|
- | rw-r--r-- | 240 | type-shadowing.m |
|
- | rw-r--r-- | 499 | type-shadowing2.m |
|
- | rw-r--r-- | 222 | uint64-model.m |
|
- | rw-r--r-- | 422 | uint64-model2.m |
|
- | rw-r--r-- | 329 | undefine-aggregate.m |
|
- | rw-r--r-- | 141 | unicode-assignment.m |
|
- | rw-r--r-- | 118 | unicode-div.m |
|
- | rw-r--r-- | 128 | unicode-div2.m |
|
- | rw-r--r-- | 168 | unicode-mul.m |
|
- | rw-r--r-- | 122 | unicode-sub.m |
|
- | rw-r--r-- | 128 | unused-record.m |
|
- | rw-r--r-- | 372 | var-case.m |
|
- | rw-r--r-- | 400 | while-stmt1.m |
|
- | rw-r--r-- | 323 | while-stmt2.m |
|
- | rw-r--r-- | 342 | while-stmt3.m |
|
- | rw-r--r-- | 178 | while-stmt4.m |
|
- | rw-r--r-- | 218 | while-stmt5.m |
|
- | rw-r--r-- | 143 | write-out-of-range.m |
|
- | rw-r--r-- | 184 | write-out-of-range2.m |
|
- | rw-r--r-- | 181 | write-out-of-range3.m |
|
- | rw-r--r-- | 639 | xml-escape-increment.m |
|
- | rw-r--r-- | 182 | xor-mixed.m |