Changes between Version 19 and Version 20 of Language
- Timestamp:
- 05/19/23 08:50:10 (3 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
Language
v19 v20 484 484 and returns an arbitrary integer in [0.''n''-1]. In verification mode, all possible choices are enumerated and explored. 485 485 486 === `$default_value`486 === Initialization by default value: `$default_value` 487 487 488 488 Assigns an object the default value of its type. Signature: … … 495 495 For example, 0 is the default value for a numeric type. 496 496 497 === `$elaborate_domain`497 === Explicit elaboration of a domain: `$elaborate_domain` 498 498 499 499 Forces explicit enumeration of the elements of a finite domain. Signature … … 503 503 In the concrete semantics, this is a no-op. 504 504 505 === `$exit`505 === Process exit: `$exit` 506 506 507 507 Terminates the calling process. Signature: … … 510 510 }}} 511 511 512 === `$havoc`512 === Assignment of arbitrary value: `$havoc` 513 513 514 514 Assigns an arbitrary value of the object's type to an object. Signature: … … 520 520 In the symbolic semantics, this function assigns a fresh symbolic constant of the appropriate type to the object pointed to by `ptr`. 521 521 522 === Hiding pointers from the reachability analyzer: `$hide`, `$hidden`, and `$reveal` 523 524 522 === Hiding pointers from the reachability analyzer: `$hide`, `$reveal`, and `$hidden` 523 524 The partial order reduction algorithm used by the CIVL Model Checker computes the set of memory locations that a process ''p'' can reach. 525 This is an analysis performed at a state. 526 The starting point of this analysis is the set of variables in the dynamic scopes referenced from ''p'''s call stack, and the ancestors of those dyscopes. 527 There is an edge from one object to another if the first contains a pointer into the second. All objects reachable from the initial objects in this directed 528 graph are the reachable objects of ''p''. 529 530 There are times when one wants to modify this directed graph by ignoring some edge. The purpose of these functions is to provide a way to do this from CIVL-C code. 531 The signatures are: 525 532 {{{ 526 533 $abstract void* $hide(const void* ptr); 534 $system void* $reveal(const void* ptr); 527 535 $system _Bool $hidden(const void* ptr); 528 $system void* $reveal(const void* ptr); 529 }}} 530 531 === `$hide` 536 }}} 537 Function `$hide` wraps a pointer object in another object which is opaque to the reachability analyzer, i.e., the analyzer will not look inside this object and therefore will not find the hidden pointer. Nothing can be done with this hidden pointer until it is "revealed", i.e., extracted from the opaque object. The function `$hidden` tells whether its argument is a value returned by `$hide`. 532 538 533 539 === `$is_derefable` … … 555 561 An error is generated if the pointer is not one that was returned by $malloc, or if it was already freed. 556 562 557 === `$pathCondition`563 === Print the path condition: `$pathCondition` 558 564 559 565 Prints the current effective path condition. … … 569 575 }}} 570 576 571 === `$reveal` 572 573 === `$wait` and `$waitall` 574 575 === `$yield` 576 577 === Waiting for process termination: `$wait` and `$waitall` 578 579 === Yielding atomicity: `$yield` 577 580 578 581 == Macros 579 582 580 581 === `$elaborate` 582 583 584 583 === Elaboration of integer value: `$elaborate` 585 584 586 585 == Contract Annotations
