[lttv.git] / trunk / verif / nico-md-merge / commit_sum.ltl

// The sum of all subbuffer commit counts must always be lower or equal
// to the writer head, because space must be reserved before it is
// written to and then committed.
// assert(write_off - _commit_sum >= 0 && write_off - _commit_sum < HALF_UCHAR);

[] (wcsum1 && wcsum2)
Commit	Line	Data
dc45444e	1	// The sum of all subbuffer commit counts must always be lower or equal
	2	// to the writer head, because space must be reserved before it is
	3	// written to and then committed.
	4	// assert(write_off - _commit_sum >= 0 && write_off - _commit_sum < HALF_UCHAR);
	5
	6	[] (wcsum1 && wcsum2)