Skip to content

A diagram the checker never read

Parts 1 through 5 were ladder, with two exceptions nobody dwelt on. This part is about the notations the suite ships and the ladder front end cannot read.

It is also the part of this site with a date on it. Everything below used to describe a tool that read nothing and said nothing about it. That defect was reported as esbmc#7354 and fixed on 28 August 2026, so the runs on this page now show the front end refusing the file by name. The lesson is kept, and rerecorded, because the interesting part was never the verdict. It was how long a corpus can carry a silent one.

An air handler permissive

A supply fan and a motorized damper. The fan may run only when the damper is open, because a fan pulling against a shut damper puts the full static pressure on the duct as vacuum and the duct can collapse. A duct smoke detector drops the fan, since a running fan distributes smoke into every zone it serves.

Three inputs, one output, one AND:

fan_cmddamper_opensmokeNOTANDfan

benchmarks/hvac/fbd_fan_damper/props.yaml
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(fan && !damper_open)"
    justification: "The fan must never run against a shut damper: the duct sees full fan static as vacuum and can collapse."
  - id: P2
    kind: invariant
    expression: "!(fan && smoke)"
    justification: "A running fan distributes smoke through the served zones, so a duct smoke alarm must drop the fan."

Two properties, one per hazard. Neither says anything about how the logic reaches its answer.

The defect

file what it is size sha256
clean.xml ladder program, PLCopen XML 4.6 KB afebdd2b2873
bomb.xml ladder program, PLCopen XML 4.2 KB daac1c0afb5f
props.yaml property file 0.4 KB ea2b1df47db4

One wire is gone. The damper_open input no longer reaches the AND block, so the fan answers to the command and the smoke detector and nothing else:

fan_cmdsmokeNOTANDfan

Both files declare the same four variables. damper_open is still an input on the interface, still named, still typed. Only the line on the drawing is missing, which is the part a variable list cannot show you.

What the ladder front end says

Recorded 2026-09-04T23:40:46Z. Every build ran the same command.

cp benchmarks/hvac/fbd_fan_damper/bomb.xml benchmarks/hvac/fbd_fan_damper/bomb.ld
esbmc benchmarks/hvac/fbd_fan_damper/bomb.ld --ld-props benchmarks/hvac/fbd_fan_damper/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:46Z.

cp benchmarks/hvac/fbd_fan_damper/bomb.xml benchmarks/hvac/fbd_fan_damper/bomb.ld
esbmc benchmarks/hvac/fbd_fan_damper/bomb.ld --ld-props benchmarks/hvac/fbd_fan_damper/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s
build ESBMC verdict expected outcome ingestion gate cpu
v8.4 8.4.0 unknown VIOLATION unknown fail 0.071 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

     1: IF !1 THEN GOTO 2
        ASSIGN fan_cmd=NONDET(_Bool);
        ASSIGN damper_open=NONDET(_Bool);
        ASSIGN smoke=NONDET(_Bool);
        GOTO 1
     2:

It stops before verification starts:

ERROR: UnsupportedConstruct(FBD body of POU 'air_handler', tier=2)
ERROR: PARSING ERROR

That is the whole answer, and it is the right one. The front end cannot read a function block diagram, so it declines the file and names the construct and the POU.

It did not always. Until #7354 was fixed, the same file came back unknown with the ingestion gate failing on fan, because the <FBD> body was discarded on the way in and what got verified was a program with no logic in it. The clean variant was worse:

Predict the verdict

This is the correct air handler. On the build this site now records, what does the ladder route report?

Answer
build verdict expected ingestion gate
v8.4 SAFE SAFE fail

Recorded 2026-09-04T23:40:46Z. Every build ran the same command.

cp benchmarks/hvac/fbd_fan_damper/clean.xml benchmarks/hvac/fbd_fan_damper/clean.ld
esbmc benchmarks/hvac/fbd_fan_damper/clean.ld --ld-props benchmarks/hvac/fbd_fan_damper/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:46Z.

cp benchmarks/hvac/fbd_fan_damper/clean.xml benchmarks/hvac/fbd_fan_damper/clean.ld
esbmc benchmarks/hvac/fbd_fan_damper/clean.ld --ld-props benchmarks/hvac/fbd_fan_damper/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s
build ESBMC verdict expected outcome ingestion gate cpu
v8.4 8.4.0 SAFE SAFE correct fail 0.014 s

v8.4 found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

     1: IF !1 THEN GOTO 2
        ASSIGN fan_cmd=NONDET(_Bool);
        ASSIGN damper_open=NONDET(_Bool);
        ASSIGN smoke=NONDET(_Bool);
        GOTO 1
     2:

It errors too, and that is the improvement. This file used to return SAFE with the gate failing, and a reader who checked only the clean row saw a verdict that matched the expectation exactly. The proof was about an empty scan loop, which satisfies every safety property ever written.

What the second route says

Recorded 2026-08-27T19:18:46Z. Every build ran the same command.

runner/record_via_c.py benchmarks/hvac/fbd_fan_damper/bomb.xml benchmarks/hvac/fbd_fan_damper/props.yaml false --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --unwind 10 --timeout 30s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build ESBMC verdict expected outcome cpu
master 8.4.0 d88a9fa4 VIOLATION VIOLATION correct 0.826 s

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  AIR_HANDLER_data__ d = {0};
  AIR_HANDLER_init__(&d, 0);
  for (int scan = 0; scan < 8; scan++) {
    __SET_VAR(d., FAN_CMD, , nondet_bool());
    __SET_VAR(d., DAMPER_OPEN, , nondet_bool());
    __SET_VAR(d., SMOKE, , nondet_bool());
    AIR_HANDLER_body__(&d);
    __ESBMC_assert(!(__GET_VAR(d.FAN,) && !__GET_VAR(d.DAMPER_OPEN,)), "P1");
    __ESBMC_assert(!(__GET_VAR(d.FAN,) && __GET_VAR(d.SMOKE,)), "P2");
  }
  return 0;
}
Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

State 1 file <generated>/harness.c line 9 column 15 function main thread 0
----------------------------------------------------
  d.FAN_CMD.value = { .FAN_CMD={ .value=(unsigned char)main::$tmp::return_value$_nondet_bool$1?1!0&0#1, .flags=0 }, .DAMPER_OPEN={ .value = 0 },
    .SMOKE={ .value = 0 }, .FAN={ .value = 0 },
    ._TMP_NOT4_OUT={ .value = 0 }, ._TMP_AND5_OUT={ .value = 0 } }

State 2 file <generated>/harness.c line 10 column 15 function main thread 0
----------------------------------------------------
  d.DAMPER_OPEN.value = { .FAN_CMD=d.FAN_CMD, .DAMPER_OPEN=0, .SMOKE=d.SMOKE, .FAN=d.FAN,
    ._TMP_NOT4_OUT=d._TMP_NOT4_OUT, ._TMP_AND5_OUT=d._TMP_AND5_OUT }

State 3 file <generated>/harness.c line 11 column 15 function main thread 0
----------------------------------------------------
  d.SMOKE.value = { .FAN_CMD=d.FAN_CMD, .DAMPER_OPEN=d.DAMPER_OPEN, .SMOKE=0,
    .FAN=d.FAN, ._TMP_NOT4_OUT=d._TMP_NOT4_OUT, ._TMP_AND5_OUT=d._TMP_AND5_OUT }

State 4 file <generated>/POUS.c line 17 column 13 function AIR_HANDLER_body__ thread 0
----------------------------------------------------
  data__->_TMP_NOT4_OUT.value = { .FAN_CMD=d.FAN_CMD, .DAMPER_OPEN=d.DAMPER_OPEN, .SMOKE=d.SMOKE,
    .FAN=d.FAN, ._TMP_NOT4_OUT=(unsigned char)(d.SMOKE.value == 0), ._TMP_AND5_OUT=d._TMP_AND5_OUT }

State 5 file $PLC_TOOLS/matiec/lib/C/iec_std_functions.h line 744 column 1 function ___AND__BOOL__BOOL thread 0
----------------------------------------------------
  op1 = 1 (00000001)

State 6 file <generated>/POUS.c line 18 column 13 function AIR_HANDLER_body__ thread 0
----------------------------------------------------
  d._TMP_AND5_OUT.value = { .FAN_CMD=d.FAN_CMD, .DAMPER_OPEN=d.DAMPER_OPEN, .SMOKE=d.SMOKE,
    .FAN=d.FAN, ._TMP_NOT4_OUT=d._TMP_NOT4_OUT, ._TMP_AND5_OUT=1 }

State 7 file <generated>/POUS.c line 24 column 13 function AIR_HANDLER_body__ thread 0
----------------------------------------------------
  data__->FAN.value = { .FAN_CMD=d.FAN_CMD, .DAMPER_OPEN=d.DAMPER_OPEN, .SMOKE=d.SMOKE,
    .FAN=d._TMP_AND5_OUT.value, ._TMP_NOT4_OUT=d._TMP_NOT4_OUT,
    ._TMP_AND5_OUT=d._TMP_AND5_OUT }

State 8 file <generated>/harness.c line 13 column 5 function main thread 0
----------------------------------------------------
Violated property:
  file <generated>/harness.c line 13 column 5 function main
  P1
  !((_Bool)((signed int)d.FAN.value) && !(_Bool)d.DAMPER_OPEN.value)


** Results:
<generated>/POUS.c, function AIR_HANDLER_body__
  PASSED       [AIR_HANDLER_body__.object-out-of-bounds.1]  line 17  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_body__.assertion.1]             line 17  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_body__.object-out-of-bounds.2]  line 17  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_body__.assertion.2]             line 17  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_body__.object-out-of-bounds.3]  line 18  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_body__.assertion.3]             line 18  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_body__.object-out-of-bounds.4]  line 18  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_body__.assertion.4]             line 18  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_body__.object-out-of-bounds.5]  line 24  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_body__.assertion.5]             line 24  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_body__.object-out-of-bounds.6]  line 24  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_body__.assertion.6]             line 24  dereference failure: Incorrect alignment when accessing data object
<generated>/POUS.c, function AIR_HANDLER_init__
  PASSED       [AIR_HANDLER_init__.object-out-of-bounds.1]  line  5  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_init__.assertion.1]             line  5  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_init__.object-out-of-bounds.2]  line  6  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_init__.assertion.2]             line  6  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_init__.object-out-of-bounds.3]  line  7  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_init__.assertion.3]             line  7  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_init__.object-out-of-bounds.4]  line  8  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_init__.assertion.4]             line  8  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_init__.object-out-of-bounds.5]  line  9  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_init__.assertion.5]             line  9  dereference failure: Incorrect alignment when accessing data object
  PASSED       [AIR_HANDLER_init__.object-out-of-bounds.6]  line 10  dereference failure: Access to object out of bounds
  PASSED       [AIR_HANDLER_init__.assertion.6]             line 10  dereference failure: Incorrect alignment when accessing data object
<generated>/harness.c, function main
  FAILED       [main.assertion.1]                           line 13  P1
  NOT CHECKED  [main.assertion.2]                           line 14  P2

** 1 of 26 properties failed, 24 passed, 1 not checked
   (this mode stops at the first violation; use --multi-property for a verdict on every property)

VIOLATION, and it names the property:

FAILED  [main.assertion.1]  line 13  P1

P1 is !(fan && !damper_open), the duct-collapse property. Beremiz rendered the function block diagram as Structured Text, MatIEC compiled that to C, and ESBMC's C front end read what the ladder front end could not. Same file, same property, same solver, opposite outcome.

The clean variant comes back SAFE on that route too, and this time it means the thing it appears to mean.

What the fix changed, and what it did not

Before, the clean air handler and the broken one produced the same word on the ladder route, and a results table would have shown two green rows. Now both produce an error, and the distinction between them lives entirely on the C route, where it always did.

Notice what the ingestion gate did across that change. It failed on these files when the tool was silent, and it fails on them now that the tool is loud. It was never measuring the verdict; it was measuring whether the property's variables were assigned inside the scan loop, and the answer to that did not move.

Two of the site's runs still fail the gate while returning a confident verdict rather than an error, and both are in lesson 7.9. That is a different defect, in a different place, and it is not yet reported.

The next lesson is the same #7354 body-dropping defect producing the opposite error.