C implicit Team1 (E-ACSL) Benchmark2

From CRV
Jump to: navigation, search

Benchmark Data

This benchmark is located in crv.liflab.ca@/home/e-acsl/crv16_benchmarks/c-implicit-track/realloc-init

The Trace Part

E-ACSL has no notion of trace

The Property Part

Informal Description

Demonstration Traces

Formal Specification

The formal property is given using the ACSL

A FO-LTL Specification