k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] Problems with input

From: Dwight Guth <dwight.guth AT runtimeverification.com>
To: Taquyeddine Zegaoui <taquyeddinezegaoui AT gmail.com>
Cc: k-user AT lists.cs.illinois.edu
Subject: Re: [[K-user] ] Problems with input
Date: Thu, 18 Aug 2016 17:33:20 -0500

Is it a requirement for you to be able to abstractly model the state of the input buffer in a way that allows for symbolic execution? If not, you may find it easier simply to use the direct IO handles in the K-IO module like #read.

On Aug 18, 2016 5:30 PM, "Taquyeddine Zegaoui" <taquyeddinezegaoui AT gmail.com> wrote:

Good morning,
I'm having considerable difficulties with implementing input behavior; using tutorials, especially IMP++, has proven uneffective as running sum-io.imp results in an endless wait. Could anyone please provide any clue regarding input ?
Thanks in advance, and sorry for the inconvenience caused.

--
ZEGAOUI Taquyeddine

[[K-user] ] Problems with input, Taquyeddine Zegaoui, 08/18/2016
- Message not available
  - Message not available
    - Re: [[K-user] ] Problems with input, Dwight Guth, 08/18/2016