test-enforce.desc

CORE
main-enforce.c
--dfcc main --enforce-contract foo
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Checks that assigns clause checking of slice expressions works as expected when 
enforcing a contract.